![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2a1i | Structured version Visualization version GIF version |
Description: Inference introducing two antecedents. Two applications of a1i 11. Inference associated with 2a1 28. (Contributed by Jeff Hankins, 4-Aug-2009.) |
Ref | Expression |
---|---|
2a1i.1 | ⊢ 𝜑 |
Ref | Expression |
---|---|
2a1i | ⊢ (𝜓 → (𝜒 → 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2a1i.1 | . . 3 ⊢ 𝜑 | |
2 | 1 | a1i 11 | . 2 ⊢ (𝜒 → 𝜑) |
3 | 2 | a1i 11 | 1 ⊢ (𝜓 → (𝜒 → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 |
This theorem is referenced by: ax13dgen3 2077 sbcrext 3761 oaordi 7975 nnaordi 8047 mapsnend 8387 cantnfval2 8928 infxpenc2lem1 9241 ackbij1lem16 9457 sornom 9499 fin23lem36 9570 isf32lem1 9575 isf32lem2 9576 zornn0g 9727 canthwe 9873 indpi 10129 seqid2 13234 swrdccatin12lem3 13936 fsum2d 14989 fsumabs 15019 fsumiun 15039 fprod2d 15198 prmodvdslcmf 16242 prmlem1a 16299 gicsubgen 18192 dmatelnd 20812 dis2ndc 21775 1stcelcls 21776 ptcmpfi 22128 caubl 23617 caublcls 23618 volsuplem 23862 cpnord 24238 fsumvma 25494 gausslemma2dlem4 25650 pntpbnd1 25867 clwwlknonex2lem2 27639 3pthdlem1 27696 frgr3vlem1 27810 3vfriswmgrlem 27814 fzto1st 30694 psgnfzto1st 30696 wl-equsal1t 34223 ax12f 35521 incssnn0 38703 lzenom 38762 clsk1independent 39759 iidn3 40254 truniALT 40294 onfrALTlem2 40299 ee220 40391 dvmptfprodlem 41660 fourierdlem89 41912 fourierdlem91 41914 sge0reuz 42161 hoi2toco 42321 linds0 43888 |
Copyright terms: Public domain | W3C validator |