Theorem 3impa 1127

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-3an 1105

This theorem is used by:  3imp  1128  3adant1  1148  3adant2  1149  ex3  1365  3impdir  1370  syl3an9b  1462  biimp3a  1498  stoic3  1806  rspec3  3285  vtocl3gaf  3544  vtocl3ga  3545  rspc3v  3597  raltpg  4664  rextpg  4665  disjiun  5097  otthg  5467  3optocl  5758  fun2ssres  6581  funtpg  6591  funssfv  6902  f1elima  7261  ot1stg  7996  ot2ndg  7997  smogt  8350  omord2  8548  omword  8551  oeword  8572  omabslem  8632  ecovass  8818  fpmg  8862  findcard  9144  endjudisj  10157  cfsmolem  10258  ingru  10804  addasspi  10884  mulasspi  10886  ltapi  10892  ltmpi  10893  axpre-ltadd  11156  leltne  11303  dedekind  11377  recextlem2  11849  divdiv32  11927  divdiv1  11930  lble  12171  fnn0ind  12699  supminf  12963  xrleltne  13174  xrmaxeq  13209  xrmineq  13210  iccgelb  13433  elicc4  13444  iccsplit  13516  elfz  13545  modabs  13942  expgt0  14136  expge0  14139  expge1  14140  mulexpz  14143  expp1z  14152  expm1  14153  expmordi  14208  digit1  14278  faclbnd4  14338  faclbnd5  14339  ccatsymb  14625  s3eqs2s1eq  14980  abssubne0  15373  binom  15889  dvds0lem  16328  dvdsnegb  16335  muldvds1  16342  muldvds2  16343  dvdscmulr  16346  dvdsmulcr  16347  divalgmodcl  16469  gcd2n0cl  16571  gcdaddm  16587  lcmdvds  16670  prmdvdsexp  16778  rpexp1i  16786  monpropd  17798  prfval  18259  xpcpropd  18268  curf2ndf  18307  eqglact  19251  ghmqusker  19361  mndodcongi  19617  oddvdsnn0  19618  efgi0  19794  efgi1  19795  efgsval2  19807  lss0cl  21077  mpofrlmd  21936  evls1fpws  22538  scmatscmid  22672  pmatcollpw3fi1lem1  22952  cnpval  23402  cnf2  23415  cnnei  23448  lfinun  23691  ptpjcn  23777  cnmptk2  23852  flfval  24156  cnmpt2plusg  24254  cnmpt2vsca  24361  ustincl  24374  xbln0  24580  blssec  24601  blpnfctr  24602  mopni2  24659  mopni3  24660  nmoval  24881  nmocl  24886  isnghm2  24890  isnmhm2  24918  cnmpt2ds  25010  metdseq0  25021  cnmpt2ip  25416  caucfil  25451  mbfimasn  25800  dvnf  26095  dvnbss  26096  coemul  26418  dvply1  26454  dvnply2  26457  pserdvlem2  26600  logeftb  26757  advlogexp  26829  cxpne0  26851  cxpp1  26854  elno2  27827  f1otrg  29229  ax5seglem9  29296  uhgrn0  29426  upgrn0  29448  upgrle  29449  uhgrwkspthlem2  30112  frgrhash2wsp  30692  sspval  31084  sspnval  31098  lnof  31116  nmooval  31124  nmooge0  31128  nmoub3i  31134  bloln  31145  nmblore  31147  hosval  32101  homval  32102  hodval  32103  hfsval  32104  hfmval  32105  homulass  32163  hoadddir  32165  nmopub2tALT  32270  nmfnleub2  32287  kbval  32315  lnopmul  32328  0lnfn  32346  lnopcoi  32364  nmcoplb  32391  nmcfnlb  32415  kbass2  32478  nmopleid  32500  hstoh  32593  mdi  32656  dmdi  32663  dmdi4  32668  tpssg  32892  fdifsuppconst  33043  supxrnemnf  33122  elrgspnlem2  33572  rloccring  33600  reofld  33672  nsgmgclem  33729  rhmimaidl  33749  dfufd2lem  33848  r1plmhm  33908  r1pquslmic  33909  lbsdiflsp0  34025  evls1fldgencl  34069  zarclsun  34269  zarclsint  34271  bnj605  35304  bnj607  35313  bnj1097  35378  fnrelpredd  35491  rankfilimb  35505  cusgredgex  35622  topdifinffinlem  38021  lindsdom  38293  lindsenlbs  38294  ftc1anclem2  38373  fzmul  38420  nninfnub  38430  exidreslem  38556  grposnOLD  38561  ghomf  38569  rngohomf  38645  rngohom1  38647  rngohomadd  38648  rngohommul  38649  rngoiso1o  38658  rngoisohom  38659  igenmin  38743  lkrcl  39894  lkrf0  39895  omlfh1N  40060  tendoex  41777  uzindd  42773  primrootsunit1  42892  sticksstones3  42943  sticksstones10  42950  sticksstones12a  42952  sticksstones12  42953  sticksstones17  42958  3anrabdioph  43541  3orrabdioph  43542  rencldnfilem  43575  dvdsabsmod0  43742  jm2.18  43743  jm2.25  43754  jm2.15nn0  43758  tfsconcatlem  44091  onsucunitp  44128  addrfv  45205  subrfv  45206  mulvfv  45207  bi3impa  45222  ssfiunibd  46056  supminfxr  46206  limsupgtlem  46519  xlimmnfv  46576  xlimpnfv  46580  dvnmul  46685  stoweidlem34  46776  stoweidlem48  46790  sge0cl  47123  sge0xp  47171  ovnsubaddlem1  47312  aovmpt4g  47966  gboge9  48557