![]() |
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 2127 sbcrext 3863 mptexgf 7234 oaordi 8567 nnaordi 8639 mapsnend 9061 cantnfval2 9694 infxpenc2lem1 10044 ackbij1lem16 10260 sornom 10302 fin23lem36 10373 isf32lem1 10378 isf32lem2 10379 zornn0g 10530 canthwe 10676 indpi 10932 seqid2 14049 pfxccatin12lem3 14718 fsum2d 15753 fsumabs 15783 fsumiun 15803 fprod2d 15961 prmodvdslcmf 17019 prmlem1a 17079 gicsubgen 19242 dmatelnd 22442 dis2ndc 23408 1stcelcls 23409 ptcmpfi 23761 caubl 25280 caublcls 25281 volsuplem 25528 cpnord 25909 fsumvma 27191 gausslemma2dlem4 27347 pntpbnd1 27564 3pthdlem1 30046 frgr3vlem1 30155 3vfriswmgrlem 30159 fzto1st 32916 psgnfzto1st 32918 wl-equsal1t 37140 ax12f 38542 incssnn0 42273 lzenom 42332 omabs2 42903 clsk1independent 43618 iidn3 44082 truniALT 44122 onfrALTlem2 44127 ee220 44219 dvmptfprodlem 45470 fourierdlem89 45721 fourierdlem91 45723 sge0reuz 45973 hoi2toco 46133 linds0 47719 |
Copyright terms: Public domain | W3C validator |