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 216	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-3an 1088

This theorem is referenced by:  3imp  1110  3adant1  1129  3adant2  1130  ex3  1345  3impdir  1350  syl3an9b  1433  biimp3a  1468  stoic3  1777  rspec3  3260  rspc3v  3582  raltpg  4644  rextpg  4645  disjiun  5074  otthg  5419  3optocl  5702  fun2ssres  6516  funtpg  6526  funssfv  6833  f1elima  7176  ot1stg  7892  ot2ndg  7893  smogt  8247  omord2  8448  omword  8451  oeword  8471  omabslem  8530  ecovass  8663  fpmg  8706  findcard  9007  endjudisj  10004  cfsmolem  10106  ingru  10651  addasspi  10731  mulasspi  10733  ltapi  10739  ltmpi  10740  axpre-ltadd  11003  leltne  11144  dedekind  11218  recextlem2  11686  divdiv32  11763  divdiv1  11766  lble  12007  fnn0ind  12499  supminf  12755  xrleltne  12959  xrmaxeq  12993  xrmineq  12994  iccgelb  13215  elicc4  13226  iccsplit  13297  elfz  13325  modabs  13704  expgt0  13896  expge0  13899  expge1  13900  mulexpz  13903  expp1z  13912  expm1  13913  expmordi  13965  digit1  14032  faclbnd4  14091  faclbnd5  14092  ccatsymb  14366  s3eqs2s1eq  14730  abssubne0  15107  binom  15621  dvds0lem  16055  dvdsnegb  16062  muldvds1  16069  muldvds2  16070  dvdscmulr  16073  dvdsmulcr  16074  divalgmodcl  16195  gcd2n0cl  16295  gcdaddm  16311  lcmdvds  16390  prmdvdsexp  16497  rpexp1i  16505  monpropd  17526  prfval  17993  xpcpropd  18003  curf2ndf  18042  eqglact  18883  mndodcongi  19227  oddvdsnn0  19228  efgi0  19401  efgi1  19402  efgsval2  19414  lss0cl  20291  mpofrlmd  21067  scmatscmid  21738  pmatcollpw3fi1lem1  22018  cnpval  22470  cnf2  22483  cnnei  22516  lfinun  22759  ptpjcn  22845  cnmptk2  22920  flfval  23224  cnmpt2plusg  23322  cnmpt2vsca  23429  ustincl  23442  xbln0  23650  blssec  23671  blpnfctr  23672  mopni2  23732  mopni3  23733  nmoval  23962  nmocl  23967  isnghm2  23971  isnmhm2  23999  cnmpt2ds  24089  metdseq0  24100  cnmpt2ip  24495  caucfil  24530  mbfimasn  24879  dvnf  25174  dvnbss  25175  coemul  25496  dvply1  25527  dvnply2  25530  pserdvlem2  25670  logeftb  25822  advlogexp  25893  cxpne0  25915  cxpp1  25918  elno2  26885  f1otrg  27368  ax5seglem9  27441  uhgrn0  27573  upgrn0  27595  upgrle  27596  uhgrwkspthlem2  28258  frgrhash2wsp  28832  sspval  29221  sspnval  29235  lnof  29253  nmooval  29261  nmooge0  29265  nmoub3i  29271  bloln  29282  nmblore  29284  hosval  30238  homval  30239  hodval  30240  hfsval  30241  hfmval  30242  homulass  30300  hoadddir  30302  nmopub2tALT  30407  nmfnleub2  30424  kbval  30452  lnopmul  30465  0lnfn  30483  lnopcoi  30501  nmcoplb  30528  nmcfnlb  30552  kbass2  30615  nmopleid  30637  hstoh  30730  mdi  30793  dmdi  30800  dmdi4  30805  fdifsuppconst  31158  supxrnemnf  31226  reofld  31682  nsgmgclem  31735  rhmimaidl  31748  lbsdiflsp0  31847  zarclsun  31960  zarclsint  31962  bnj605  33026  bnj607  33035  bnj1097  33100  fnrelpredd  33200  cusgredgex  33222  topdifinffinlem  35590  lindsdom  35843  lindsenlbs  35844  ftc1anclem2  35923  fzmul  35971  nninfnub  35981  exidreslem  36107  grposnOLD  36112  ghomf  36120  rngohomf  36196  rngohom1  36198  rngohomadd  36199  rngohommul  36200  rngoiso1o  36209  rngoisohom  36210  igenmin  36294  lkrcl  37326  lkrf0  37327  omlfh1N  37492  tendoex  39210  uzindd  40206  sticksstones3  40328  sticksstones10  40335  sticksstones12a  40337  sticksstones12  40338  sticksstones17  40343  3anrabdioph  40820  3orrabdioph  40821  rencldnfilem  40858  dvdsabsmod0  41026  jm2.18  41027  jm2.25  41038  jm2.15nn0  41042  addrfv  42321  subrfv  42322  mulvfv  42323  bi3impa  42338  ssfiunibd  43097  supminfxr  43253  limsupgtlem  43568  xlimmnfv  43625  xlimpnfv  43629  dvnmul  43734  stoweidlem34  43825  stoweidlem48  43839  sge0cl  44170  sge0xp  44218  ovnsubaddlem1  44359  aovmpt4g  44958  gboge9  45481