![]() |
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 125 ancl 540 ancr 542 anc2r 550 hbim1 2272 ralimia 3132 ceqsalgALT 3433 rspct 3504 elabgt 3553 fvmptt 6563 tfi 7333 fnfi 8528 finsschain 8563 ordiso2 8711 ordtypelem7 8720 dfom3 8843 infdiffi 8854 cantnfp1lem3 8876 cantnf 8889 r1ordg 8940 ttukeylem6 9673 fpwwe2lem8 9796 wunfi 9880 dfnn2 11393 trclfvcotr 14161 psgnunilem3 18304 pgpfac1 18870 fiuncmp 21620 filssufilg 22127 ufileu 22135 pjnormssi 29603 bnj1110 31653 waj-ax 33000 bj-sb 33270 bj-equsal1 33390 bj-equsal2 33391 rdgeqoa 33816 wl-mps 33888 refimssco 38880 atbiffatnnb 42016 elsetrecslem 43560 |
Copyright terms: Public domain | W3C validator |