| 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 544 ancr 546 anc2r 554 hbim1 2297 ralimia 3080 ceqsalgALT 3518 rspct 3608 fvmptt 7036 tfi 7874 fnfi 9218 imafiOLD 9354 finsschain 9399 ordiso2 9555 ordtypelem7 9564 dfom3 9687 infdiffi 9698 cantnfp1lem3 9720 cantnf 9733 r1ordg 9818 ttukeylem6 10554 fpwwe2lem7 10677 wunfi 10761 dfnn2 12279 trclfvcotr 15048 psgnunilem3 19514 pgpfac1 20100 fiuncmp 23412 filssufilg 23919 ufileu 23927 dfn0s2 28336 pjnormssi 32187 bnj1110 34996 waj-ax 36415 bj-nnclav 36547 bj-sb 36688 bj-equsal1 36825 bj-equsal2 36826 rdgeqoa 37371 wl-mps 37508 refimssco 43620 dfbi1ALTa 44960 simprimi 44961 natlocalincr 46891 atbiffatnnb 46924 rexrsb 47112 elsetrecslem 49218 |
| Copyright terms: Public domain | W3C validator |