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.18OLD 129 ancl 545 ancr 547 anc2r 555 hbim1 2297 ralimia 3158 ceqsalgALT 3531 rspct 3608 elabgt 3662 fvmptt 6781 tfi 7556 fnfi 8785 finsschain 8820 ordiso2 8968 ordtypelem7 8977 dfom3 9099 infdiffi 9110 cantnfp1lem3 9132 cantnf 9145 r1ordg 9196 ttukeylem6 9925 fpwwe2lem8 10048 wunfi 10132 dfnn2 11640 trclfvcotr 14359 psgnunilem3 18555 pgpfac1 19133 fiuncmp 21942 filssufilg 22449 ufileu 22457 pjnormssi 29873 bnj1110 32152 waj-ax 33660 bj-nnclav 33782 bj-peircestab 33786 bj-sb 33919 bj-equsal1 34045 bj-equsal2 34046 rdgeqoa 34534 wl-mps 34630 refimssco 39847 atbiffatnnb 43029 elsetrecslem 44699 |
Copyright terms: Public domain | W3C validator |