![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > a2i | Structured version Visualization version GIF version |
Description: Inference distributing an antecedent. Inference associated with ax-2 7. Its associated inference is mpd 15. (Contributed by NM, 29-Dec-1992.) |
Ref | Expression |
---|---|
a2i.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
a2i | ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | a2i.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | ax-2 7 | . 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-2 7 |
This theorem is referenced by: mpd 15 imim2i 16 sylcom 30 pm2.43 56 pm2.18 122 ancl 568 ancr 571 anc2r 578 hbim1 2163 hbim1OLD 2263 ralimia 2979 ceqsalgALT 3262 rspct 3333 elabgt 3379 fvmptt 6339 tfi 7095 fnfi 8279 finsschain 8314 ordiso2 8461 ordtypelem7 8470 dfom3 8582 infdiffi 8593 cantnfp1lem3 8615 cantnf 8628 r1ordg 8679 ttukeylem6 9374 fpwwe2lem8 9497 wunfi 9581 dfnn2 11071 trclfvcotr 13794 psgnunilem3 17962 pgpfac1 18525 fiuncmp 21255 filssufilg 21762 ufileu 21770 pjnormssi 29155 bnj1110 31176 waj-ax 32538 bj-sb 32802 bj-equsal1 32936 bj-equsal2 32937 rdgeqoa 33348 wl-mps 33420 refimssco 38230 atbiffatnnb 41400 elsetrecslem 42770 |
Copyright terms: Public domain | W3C validator |