Theorem 3impa 1194

Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)

Hypothesis

Ref	Expression
3impa.1	|- ( ( ( ph /\ ps ) /\ ch ) -> th )

Assertion

Ref	Expression
3impa	|- ( ( ph /\ ps /\ ch ) -> th )

Proof of Theorem 3impa

Step	Hyp	Ref	Expression
1		3impa.1	. . 3 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
2	1	exp31 364	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	3imp 1193	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 978

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  ex3  1195  3impdir  1294  syl3an9b  1310  biimp3a  1345  stoic3  1431  rspec3  2567  rspc3v  2857  raltpg  3645  rextpg  3646  disjiun  3998  otexg  4230  opelopabt  4262  tpexg  4444  3optocl  4704  fun2ssres  5259  funssfv  5541  fvun1  5582  foco2  5754  f1elima  5773  eloprabga  5961  caovimo  6067  ot1stg  6152  ot2ndg  6153  ot3rdgg  6154  brtposg  6254  rdgexggg  6377  rdgivallem  6381  nnmass  6487  nndir  6490  nnaword  6511  th3q  6639  ecovass  6643  ecoviass  6644  fpmg  6673  findcard  6887  unfiin  6924  addasspig  7328  mulasspig  7330  mulcanpig  7333  ltapig  7336  ltmpig  7337  addassnqg  7380  ltbtwnnqq  7413  mulnnnq0  7448  addassnq0  7460  genpassl  7522  genpassu  7523  genpassg  7524  aptiprleml  7637  adddir  7947  le2tri3i  8065  addsub12  8169  subdir  8342  reapmul1  8551  recexaplem2  8608  div12ap  8650  divdiv32ap  8676  divdivap1  8679  lble  8903  zaddcllemneg  9291  fnn0ind  9368  xrltso  9795  iccgelb  9931  elicc4  9939  elfz  10013  fzrevral  10104  expnegap0  10527  expgt0  10552  expge0  10555  expge1  10556  mulexpzap  10559  expp1zap  10568  expm1ap  10569  apexp1  10697  abssubap0  11098  binom  11491  dvds0lem  11807  dvdsnegb  11814  muldvds1  11822  muldvds2  11823  divalgmodcl  11932  gcd2n0cl  11969  lcmdvds  12078  prmdvdsexp  12147  rpexp1i  12153  eqglact  13082  cnpval  13668  cnf2  13675  cnnei  13702  blssec  13908  blpnfctr  13909  mopni2  13953  mopni3  13954