![]() |
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 123 ancl 528 ancr 530 anc2r 538 hbim1 2289 hbim1OLD 2389 ralimia 3099 ceqsalgALT 3383 rspct 3454 elabgt 3499 fvmptt 6443 tfi 7201 fnfi 8395 finsschain 8430 ordiso2 8577 ordtypelem7 8586 dfom3 8709 infdiffi 8720 cantnfp1lem3 8742 cantnf 8755 r1ordg 8806 ttukeylem6 9539 fpwwe2lem8 9662 wunfi 9746 dfnn2 11236 trclfvcotr 13959 psgnunilem3 18124 pgpfac1 18688 fiuncmp 21429 filssufilg 21936 ufileu 21944 pjnormssi 29368 bnj1110 31389 waj-ax 32751 bj-sb 33015 bj-equsal1 33147 bj-equsal2 33148 rdgeqoa 33556 wl-mps 33628 refimssco 38440 atbiffatnnb 41600 elsetrecslem 42974 |
Copyright terms: Public domain | W3C validator |