Theorem 3impa 1108

Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3imp 1109 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 1087	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3impa.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 216	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-3an 1087

This theorem is referenced by:  3imp  1109  3adant1  1128  3adant2  1129  ex3  1344  3impdir  1349  syl3an9b  1432  biimp3a  1467  stoic3  1780  rspec3  3135  rspc3v  3565  raltpg  4631  rextpg  4632  disjiun  5057  otthg  5394  3optocl  5673  fun2ssres  6463  funtpg  6473  funssfv  6777  f1elima  7117  ot1stg  7818  ot2ndg  7819  smogt  8169  omord2  8360  omword  8363  oeword  8383  omabslem  8440  ecovass  8571  fpmg  8614  findcard  8908  endjudisj  9855  cfsmolem  9957  ingru  10502  addasspi  10582  mulasspi  10584  ltapi  10590  ltmpi  10591  axpre-ltadd  10854  leltne  10995  dedekind  11068  recextlem2  11536  divdiv32  11613  divdiv1  11616  lble  11857  fnn0ind  12349  supminf  12604  xrleltne  12808  xrmaxeq  12842  xrmineq  12843  iccgelb  13064  elicc4  13075  iccsplit  13146  elfz  13174  modabs  13552  expgt0  13744  expge0  13747  expge1  13748  mulexpz  13751  expp1z  13760  expm1  13761  expmordi  13813  digit1  13880  faclbnd4  13939  faclbnd5  13940  ccatsymb  14215  s3eqs2s1eq  14579  abssubne0  14956  binom  15470  dvds0lem  15904  dvdsnegb  15911  muldvds1  15918  muldvds2  15919  dvdscmulr  15922  dvdsmulcr  15923  divalgmodcl  16044  gcd2n0cl  16144  gcdaddm  16160  lcmdvds  16241  prmdvdsexp  16348  rpexp1i  16356  monpropd  17366  prfval  17832  xpcpropd  17842  curf2ndf  17881  eqglact  18722  mndodcongi  19066  oddvdsnn0  19067  efgi0  19241  efgi1  19242  efgsval2  19254  lss0cl  20123  mpofrlmd  20894  scmatscmid  21563  pmatcollpw3fi1lem1  21843  cnpval  22295  cnf2  22308  cnnei  22341  lfinun  22584  ptpjcn  22670  cnmptk2  22745  flfval  23049  cnmpt2plusg  23147  cnmpt2vsca  23254  ustincl  23267  xbln0  23475  blssec  23496  blpnfctr  23497  mopni2  23555  mopni3  23556  nmoval  23785  nmocl  23790  isnghm2  23794  isnmhm2  23822  cnmpt2ds  23912  metdseq0  23923  cnmpt2ip  24317  caucfil  24352  mbfimasn  24701  dvnf  24996  dvnbss  24997  coemul  25318  dvply1  25349  dvnply2  25352  pserdvlem2  25492  logeftb  25644  advlogexp  25715  cxpne0  25737  cxpp1  25740  f1otrg  27136  ax5seglem9  27208  uhgrn0  27340  upgrn0  27362  upgrle  27363  uhgrwkspthlem2  28023  frgrhash2wsp  28597  sspval  28986  sspnval  29000  lnof  29018  nmooval  29026  nmooge0  29030  nmoub3i  29036  bloln  29047  nmblore  29049  hosval  30003  homval  30004  hodval  30005  hfsval  30006  hfmval  30007  homulass  30065  hoadddir  30067  nmopub2tALT  30172  nmfnleub2  30189  kbval  30217  lnopmul  30230  0lnfn  30248  lnopcoi  30266  nmcoplb  30293  nmcfnlb  30317  kbass2  30380  nmopleid  30402  hstoh  30495  mdi  30558  dmdi  30565  dmdi4  30570  fdifsuppconst  30925  supxrnemnf  30993  reofld  31446  nsgmgclem  31498  rhmimaidl  31511  lbsdiflsp0  31609  zarclsun  31722  zarclsint  31724  bnj605  32787  bnj607  32796  bnj1097  32861  fnrelpredd  32961  cusgredgex  32983  elno2  33784  topdifinffinlem  35445  lindsdom  35698  lindsenlbs  35699  ftc1anclem2  35778  fzmul  35826  nninfnub  35836  exidreslem  35962  grposnOLD  35967  ghomf  35975  rngohomf  36051  rngohom1  36053  rngohomadd  36054  rngohommul  36055  rngoiso1o  36064  rngoisohom  36065  igenmin  36149  lkrcl  37033  lkrf0  37034  omlfh1N  37199  tendoex  38916  uzindd  39913  sticksstones3  40032  sticksstones10  40039  sticksstones12a  40041  sticksstones12  40042  sticksstones17  40047  3anrabdioph  40520  3orrabdioph  40521  rencldnfilem  40558  dvdsabsmod0  40725  jm2.18  40726  jm2.25  40737  jm2.15nn0  40741  addrfv  41976  subrfv  41977  mulvfv  41978  bi3impa  41993  ssfiunibd  42738  supminfxr  42894  limsupgtlem  43208  xlimmnfv  43265  xlimpnfv  43269  dvnmul  43374  stoweidlem34  43465  stoweidlem48  43479  sge0cl  43809  sge0xp  43857  ovnsubaddlem1  43998  aovmpt4g  44580  gboge9  45104