![]() |
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 2171 sbcrext 3661 oaordi 7784 nnaordi 7856 cantnfval2 8734 infxpenc2lem1 9046 ackbij1lem16 9263 sornom 9305 fin23lem36 9376 isf32lem1 9381 isf32lem2 9382 zornn0g 9533 canthwe 9679 indpi 9935 seqid2 13054 swrdccatin12lem3 13699 fsum2d 14710 fsumabs 14740 fsumiun 14760 fprod2d 14918 prmodvdslcmf 15958 prmlem1a 16020 gicsubgen 17928 dmatelnd 20520 dis2ndc 21484 1stcelcls 21485 ptcmpfi 21837 caubl 23325 caublcls 23326 volsuplem 23543 cpnord 23918 fsumvma 25159 gausslemma2dlem4 25315 pntpbnd1 25496 clwwlknonex2lem2 27284 3pthdlem1 27344 frgr3vlem1 27455 3vfriswmgrlem 27459 fzto1st 30193 psgnfzto1st 30195 wl-equsal1t 33661 ax12f 34746 incssnn0 37798 lzenom 37857 clsk1independent 38868 iidn3 39230 truniALT 39274 onfrALTlem2 39284 ee220 39386 dvmptfprodlem 40672 fourierdlem89 40924 fourierdlem91 40926 sge0reuz 41176 hoi2toco 41336 linds0 42777 |
Copyright terms: Public domain | W3C validator |