Theorem 2a1i 12

Description: Inference introducing two antecedents. Two applications of a1i 11. Inference associated with 2a1 28. (Contributed by Jeff Hankins, 4-Aug-2009.)

Hypothesis

Ref	Expression
2a1i.1	|- ph

Assertion

Ref	Expression
2a1i	|- ( ps -> ( ch -> ph ) )

Proof of Theorem 2a1i

Step	Hyp	Ref	Expression
1		2a1i.1	. . 3 |- ph
2	1	a1i 11	. 2 |- ( ch -> ph )
3	2	a1i 11	1 |- ( ps -> ( ch -> ph ) )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6

This theorem is referenced by:  ax13dgen3  2016  sbcrext  3511  sbcrextOLD  3512  oaordi  7626  nnaordi  7698  map1  8036  cantnfval2  8566  infxpenc2lem1  8842  ackbij1lem16  9057  sornom  9099  fin23lem36  9170  isf32lem1  9175  isf32lem2  9176  zornn0g  9327  canthwe  9473  indpi  9729  seqid2  12847  swrdccatin12lem3  13490  fsum2d  14502  fsumabs  14533  fsumiun  14553  fprod2d  14711  prmodvdslcmf  15751  prmlem1a  15813  gicsubgen  17721  dmatelnd  20302  dis2ndc  21263  1stcelcls  21264  ptcmpfi  21616  caubl  23106  caublcls  23107  volsuplem  23323  cpnord  23698  fsumvma  24938  gausslemma2dlem4  25094  pntpbnd1  25275  3pthdlem1  27024  frgr3vlem1  27137  3vfriswmgrlem  27141  numclwwlkovf2exlem2  27212  fzto1st  29853  psgnfzto1st  29855  wl-equsal1t  33327  ax12f  34225  incssnn0  37274  lzenom  37333  clsk1independent  38344  iidn3  38707  truniALT  38751  onfrALTlem2  38761  ee220  38863  dvmptfprodlem  40159  fourierdlem89  40412  fourierdlem91  40414  sge0reuz  40664  hoi2toco  40821  linds0  42254