![]() |
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 ancl 543 ancr 545 anc2r 553 hbim1 2287 ralimia 3070 ceqsalgALT 3499 rspct 3594 elabgtOLDOLD 3661 fvmptt 7031 tfi 7865 fnfi 9217 imafiOLD 9358 finsschain 9405 ordiso2 9560 ordtypelem7 9569 dfom3 9692 infdiffi 9703 cantnfp1lem3 9725 cantnf 9738 r1ordg 9823 ttukeylem6 10559 fpwwe2lem7 10682 wunfi 10766 dfnn2 12279 trclfvcotr 15016 psgnunilem3 19496 pgpfac1 20082 fiuncmp 23402 filssufilg 23909 ufileu 23917 dfn0s2 28307 pjnormssi 32104 bnj1110 34829 waj-ax 36128 bj-nnclav 36251 bj-sb 36394 bj-equsal1 36531 bj-equsal2 36532 rdgeqoa 37079 wl-mps 37204 refimssco 43292 natlocalincr 46513 atbiffatnnb 46545 rexrsb 46731 elsetrecslem 48463 |
Copyright terms: Public domain | W3C validator |