Theorem 3impa 1109

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

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

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 207  df-3an 1088

This theorem is referenced by:  3imp  1110  3adant1  1130  3adant2  1131  ex3  1347  3impdir  1352  syl3an9b  1436  biimp3a  1471  stoic3  1777  rspec3  3252  vtocl3gaf  3532  vtocl3ga  3534  rspc3v  3588  raltpg  4648  rextpg  4649  disjiun  5077  otthg  5423  3optocl  5711  fun2ssres  6526  funtpg  6536  funssfv  6843  f1elima  7197  ot1stg  7935  ot2ndg  7936  smogt  8287  omord2  8482  omword  8485  oeword  8505  omabslem  8565  ecovass  8748  fpmg  8792  findcard  9073  endjudisj  10060  cfsmolem  10161  ingru  10706  addasspi  10786  mulasspi  10788  ltapi  10794  ltmpi  10795  axpre-ltadd  11058  leltne  11202  dedekind  11276  recextlem2  11748  divdiv32  11829  divdiv1  11832  lble  12074  fnn0ind  12572  supminf  12833  xrleltne  13044  xrmaxeq  13078  xrmineq  13079  iccgelb  13302  elicc4  13313  iccsplit  13385  elfz  13413  modabs  13808  expgt0  14002  expge0  14005  expge1  14006  mulexpz  14009  expp1z  14018  expm1  14019  expmordi  14074  digit1  14144  faclbnd4  14204  faclbnd5  14205  ccatsymb  14490  s3eqs2s1eq  14845  abssubne0  15224  binom  15737  dvds0lem  16177  dvdsnegb  16184  muldvds1  16191  muldvds2  16192  dvdscmulr  16195  dvdsmulcr  16196  divalgmodcl  16318  gcd2n0cl  16420  gcdaddm  16436  lcmdvds  16519  prmdvdsexp  16626  rpexp1i  16634  monpropd  17644  prfval  18105  xpcpropd  18114  curf2ndf  18153  eqglact  19091  ghmqusker  19199  mndodcongi  19455  oddvdsnn0  19456  efgi0  19632  efgi1  19633  efgsval2  19645  lss0cl  20880  mpofrlmd  21714  evls1fpws  22284  scmatscmid  22421  pmatcollpw3fi1lem1  22701  cnpval  23151  cnf2  23164  cnnei  23197  lfinun  23440  ptpjcn  23526  cnmptk2  23601  flfval  23905  cnmpt2plusg  24003  cnmpt2vsca  24110  ustincl  24123  xbln0  24329  blssec  24350  blpnfctr  24351  mopni2  24408  mopni3  24409  nmoval  24630  nmocl  24635  isnghm2  24639  isnmhm2  24667  cnmpt2ds  24759  metdseq0  24770  cnmpt2ip  25175  caucfil  25210  mbfimasn  25560  dvnf  25856  dvnbss  25857  coemul  26184  dvply1  26218  dvnply2  26222  pserdvlem2  26365  logeftb  26519  advlogexp  26591  cxpne0  26613  cxpp1  26616  elno2  27593  f1otrg  28849  ax5seglem9  28915  uhgrn0  29045  upgrn0  29067  upgrle  29068  uhgrwkspthlem2  29732  frgrhash2wsp  30312  sspval  30703  sspnval  30717  lnof  30735  nmooval  30743  nmooge0  30747  nmoub3i  30753  bloln  30764  nmblore  30766  hosval  31720  homval  31721  hodval  31722  hfsval  31723  hfmval  31724  homulass  31782  hoadddir  31784  nmopub2tALT  31889  nmfnleub2  31906  kbval  31934  lnopmul  31947  0lnfn  31965  lnopcoi  31983  nmcoplb  32010  nmcfnlb  32034  kbass2  32097  nmopleid  32119  hstoh  32212  mdi  32275  dmdi  32282  dmdi4  32287  tpssg  32517  fdifsuppconst  32670  supxrnemnf  32751  elrgspnlem2  33210  rloccring  33237  reofld  33308  nsgmgclem  33376  rhmimaidl  33397  dfufd2lem  33514  r1plmhm  33570  r1pquslmic  33571  lbsdiflsp0  33639  evls1fldgencl  33683  zarclsun  33883  zarclsint  33885  bnj605  34919  bnj607  34928  bnj1097  34993  fnrelpredd  35102  rankfilimb  35113  cusgredgex  35166  topdifinffinlem  37391  lindsdom  37664  lindsenlbs  37665  ftc1anclem2  37744  fzmul  37791  nninfnub  37801  exidreslem  37927  grposnOLD  37932  ghomf  37940  rngohomf  38016  rngohom1  38018  rngohomadd  38019  rngohommul  38020  rngoiso1o  38029  rngoisohom  38030  igenmin  38114  lkrcl  39201  lkrf0  39202  omlfh1N  39367  tendoex  41084  uzindd  42080  primrootsunit1  42200  sticksstones3  42251  sticksstones10  42258  sticksstones12a  42260  sticksstones12  42261  sticksstones17  42266  3anrabdioph  42885  3orrabdioph  42886  rencldnfilem  42923  dvdsabsmod0  43090  jm2.18  43091  jm2.25  43102  jm2.15nn0  43106  tfsconcatlem  43439  onsucunitp  43476  addrfv  44571  subrfv  44572  mulvfv  44573  bi3impa  44588  ssfiunibd  45420  supminfxr  45572  limsupgtlem  45885  xlimmnfv  45942  xlimpnfv  45946  dvnmul  46051  stoweidlem34  46142  stoweidlem48  46156  sge0cl  46489  sge0xp  46537  ovnsubaddlem1  46678  aovmpt4g  47311  gboge9  47874