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 54 pm2.18 121 ancl 567 ancr 570 anc2r 577 hbim1 2110 hbim1OLD 2215 ralimia 2934 ceqsalgALT 3204 rspct 3275 elabgt 3316 fvmptt 6208 tfi 6945 fnfi 8123 finsschain 8156 ordiso2 8303 ordtypelem7 8312 dfom3 8427 infdiffi 8438 cantnfp1lem3 8460 cantnf 8473 r1ordg 8524 ttukeylem6 9219 fpwwe2lem8 9338 wunfi 9422 dfnn2 10910 trclfvcotr 13598 psgnunilem3 17739 pgpfac1 18302 fiuncmp 21017 filssufilg 21525 ufileu 21533 pjnormssi 28411 bnj1110 30304 waj-ax 31583 bj-sb 31864 bj-equsal1 31999 bj-equsal2 32000 rdgeqoa 32394 wl-mps 32469 refimssco 36932 atbiffatnnb 39728 elsetrecslem 42243 |
Copyright terms: Public domain | W3C validator |