| 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 2139 sbcrext 3873 mptexgf 7242 oaordi 8584 nnaordi 8656 mapsnend 9076 cantnfval2 9709 infxpenc2lem1 10059 ackbij1lem16 10274 sornom 10317 fin23lem36 10388 isf32lem1 10393 isf32lem2 10394 zornn0g 10545 canthwe 10691 indpi 10947 seqid2 14089 pfxccatin12lem3 14770 fsum2d 15807 fsumabs 15837 fsumiun 15857 fprod2d 16017 prmodvdslcmf 17085 prmlem1a 17144 gicsubgen 19297 dmatelnd 22502 dis2ndc 23468 1stcelcls 23469 ptcmpfi 23821 caubl 25342 caublcls 25343 volsuplem 25590 cpnord 25971 fsumvma 27257 gausslemma2dlem4 27413 pntpbnd1 27630 3pthdlem1 30183 frgr3vlem1 30292 3vfriswmgrlem 30296 fzto1st 33123 psgnfzto1st 33125 wl-equsal1t 37543 ax12f 38941 incssnn0 42722 lzenom 42781 omabs2 43345 clsk1independent 44059 iidn3 44521 truniALT 44561 onfrALTlem2 44566 ee220 44658 dvmptfprodlem 45959 dvnprodlem1 45961 fourierdlem89 46210 fourierdlem91 46212 sge0reuz 46462 hoi2toco 46622 linds0 48382 |
| Copyright terms: Public domain | W3C validator |