Theorem 3impa 1115

Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3imp 1116 by Wolf Lammen, 20-Jun-2022.)

Hypothesis

Ref	Expression
3impa.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3impa	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impa

Step	Hyp	Ref	Expression
1		df-3an 1094	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3impa.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 218	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208  df-3an 1094

This theorem is referenced by:  3imp  1116  3adant1  1136  3adant2  1137  ex3  1353  3impdir  1358  syl3an9b  1442  biimp3a  1477  stoic3  1783  rspec3  3259  vtocl3gaf  3523  vtocl3ga  3524  rspc3v  3576  raltpg  4631  rextpg  4632  disjiun  5061  otthg  5426  3optocl  5716  fun2ssres  6531  funtpg  6541  funssfv  6849  f1elima  7208  ot1stg  7946  ot2ndg  7947  smogt  8298  omord2  8493  omword  8496  oeword  8517  omabslem  8577  ecovass  8762  fpmg  8807  findcard  9089  endjudisj  10083  cfsmolem  10184  ingru  10730  addasspi  10810  mulasspi  10812  ltapi  10818  ltmpi  10819  axpre-ltadd  11082  leltne  11227  dedekind  11301  recextlem2  11773  divdiv32  11855  divdiv1  11858  lble  12100  fnn0ind  12620  supminf  12877  xrleltne  13088  xrmaxeq  13123  xrmineq  13124  iccgelb  13347  elicc4  13358  iccsplit  13430  elfz  13459  modabs  13855  expgt0  14049  expge0  14052  expge1  14053  mulexpz  14056  expp1z  14065  expm1  14066  expmordi  14121  digit1  14191  faclbnd4  14251  faclbnd5  14252  ccatsymb  14537  s3eqs2s1eq  14892  abssubne0  15271  binom  15787  dvds0lem  16227  dvdsnegb  16234  muldvds1  16241  muldvds2  16242  dvdscmulr  16245  dvdsmulcr  16246  divalgmodcl  16368  gcd2n0cl  16470  gcdaddm  16486  lcmdvds  16569  prmdvdsexp  16677  rpexp1i  16685  monpropd  17696  prfval  18157  xpcpropd  18166  curf2ndf  18205  eqglact  19146  ghmqusker  19254  mndodcongi  19510  oddvdsnn0  19511  efgi0  19687  efgi1  19688  efgsval2  19700  lss0cl  20938  mpofrlmd  21753  evls1fpws  22356  scmatscmid  22490  pmatcollpw3fi1lem1  22770  cnpval  23220  cnf2  23233  cnnei  23266  lfinun  23509  ptpjcn  23595  cnmptk2  23670  flfval  23974  cnmpt2plusg  24072  cnmpt2vsca  24179  ustincl  24192  xbln0  24398  blssec  24419  blpnfctr  24420  mopni2  24477  mopni3  24478  nmoval  24699  nmocl  24704  isnghm2  24708  isnmhm2  24736  cnmpt2ds  24828  metdseq0  24839  cnmpt2ip  25234  caucfil  25269  mbfimasn  25618  dvnf  25913  dvnbss  25914  coemul  26236  dvply1  26269  dvnply2  26272  pserdvlem2  26412  logeftb  26566  advlogexp  26638  cxpne0  26660  cxpp1  26663  elno2  27637  f1otrg  28958  ax5seglem9  29025  uhgrn0  29155  upgrn0  29177  upgrle  29178  uhgrwkspthlem2  29841  frgrhash2wsp  30421  sspval  30813  sspnval  30827  lnof  30845  nmooval  30853  nmooge0  30857  nmoub3i  30863  bloln  30874  nmblore  30876  hosval  31830  homval  31831  hodval  31832  hfsval  31833  hfmval  31834  homulass  31892  hoadddir  31894  nmopub2tALT  31999  nmfnleub2  32016  kbval  32044  lnopmul  32057  0lnfn  32075  lnopcoi  32093  nmcoplb  32120  nmcfnlb  32144  kbass2  32207  nmopleid  32229  hstoh  32322  mdi  32385  dmdi  32392  dmdi4  32397  tpssg  32626  fdifsuppconst  32782  supxrnemnf  32861  elrgspnlem2  33325  rloccring  33352  reofld  33427  nsgmgclem  33495  rhmimaidl  33516  dfufd2lem  33641  r1plmhm  33702  r1pquslmic  33703  lbsdiflsp0  33819  evls1fldgencl  33863  zarclsun  34063  zarclsint  34065  bnj605  35098  bnj607  35107  bnj1097  35172  fnrelpredd  35281  rankfilimb  35292  cusgredgex  35359  topdifinffinlem  37718  lindsdom  37990  lindsenlbs  37991  ftc1anclem2  38070  fzmul  38117  nninfnub  38127  exidreslem  38253  grposnOLD  38258  ghomf  38266  rngohomf  38342  rngohom1  38344  rngohomadd  38345  rngohommul  38346  rngoiso1o  38355  rngoisohom  38356  igenmin  38440  lkrcl  39593  lkrf0  39594  omlfh1N  39759  tendoex  41476  uzindd  42472  primrootsunit1  42591  sticksstones3  42642  sticksstones10  42649  sticksstones12a  42651  sticksstones12  42652  sticksstones17  42657  3anrabdioph  43240  3orrabdioph  43241  rencldnfilem  43274  dvdsabsmod0  43441  jm2.18  43442  jm2.25  43453  jm2.15nn0  43457  tfsconcatlem  43790  onsucunitp  43827  addrfv  44921  subrfv  44922  mulvfv  44923  bi3impa  44938  ssfiunibd  45765  supminfxr  45915  limsupgtlem  46228  xlimmnfv  46285  xlimpnfv  46289  dvnmul  46394  stoweidlem34  46485  stoweidlem48  46499  sge0cl  46832  sge0xp  46880  ovnsubaddlem1  47021  aovmpt4g  47672  gboge9  48263