Theorem 3impa 1110

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

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

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 1089

This theorem is referenced by:  3imp  1111  3adant1  1130  3adant2  1131  ex3  1346  3impdir  1351  syl3an9b  1434  biimp3a  1469  stoic3  1774  rspec3  3286  vtocl3gaf  3593  vtocl3ga  3595  rspc3v  3651  raltpg  4723  rextpg  4724  disjiun  5154  otthg  5505  3optocl  5796  fun2ssres  6623  funtpg  6633  funssfv  6941  f1elima  7300  ot1stg  8044  ot2ndg  8045  smogt  8423  omord2  8623  omword  8626  oeword  8646  omabslem  8706  ecovass  8882  fpmg  8926  findcard  9229  endjudisj  10238  cfsmolem  10339  ingru  10884  addasspi  10964  mulasspi  10966  ltapi  10972  ltmpi  10973  axpre-ltadd  11236  leltne  11379  dedekind  11453  recextlem2  11921  divdiv32  12002  divdiv1  12005  lble  12247  fnn0ind  12742  supminf  13000  xrleltne  13207  xrmaxeq  13241  xrmineq  13242  iccgelb  13463  elicc4  13474  iccsplit  13545  elfz  13573  modabs  13955  expgt0  14146  expge0  14149  expge1  14150  mulexpz  14153  expp1z  14162  expm1  14163  expmordi  14217  digit1  14286  faclbnd4  14346  faclbnd5  14347  ccatsymb  14630  s3eqs2s1eq  14987  abssubne0  15365  binom  15878  dvds0lem  16315  dvdsnegb  16322  muldvds1  16329  muldvds2  16330  dvdscmulr  16333  dvdsmulcr  16334  divalgmodcl  16455  gcd2n0cl  16555  gcdaddm  16571  lcmdvds  16655  prmdvdsexp  16762  rpexp1i  16770  monpropd  17798  prfval  18268  xpcpropd  18278  curf2ndf  18317  eqglact  19219  ghmqusker  19327  mndodcongi  19585  oddvdsnn0  19586  efgi0  19762  efgi1  19763  efgsval2  19775  lss0cl  20968  mpofrlmd  21820  evls1fpws  22394  scmatscmid  22533  pmatcollpw3fi1lem1  22813  cnpval  23265  cnf2  23278  cnnei  23311  lfinun  23554  ptpjcn  23640  cnmptk2  23715  flfval  24019  cnmpt2plusg  24117  cnmpt2vsca  24224  ustincl  24237  xbln0  24445  blssec  24466  blpnfctr  24467  mopni2  24527  mopni3  24528  nmoval  24757  nmocl  24762  isnghm2  24766  isnmhm2  24794  cnmpt2ds  24884  metdseq0  24895  cnmpt2ip  25301  caucfil  25336  mbfimasn  25686  dvnf  25983  dvnbss  25984  coemul  26311  dvply1  26343  dvnply2  26347  pserdvlem2  26490  logeftb  26643  advlogexp  26715  cxpne0  26737  cxpp1  26740  elno2  27717  f1otrg  28897  ax5seglem9  28970  uhgrn0  29102  upgrn0  29124  upgrle  29125  uhgrwkspthlem2  29790  frgrhash2wsp  30364  sspval  30755  sspnval  30769  lnof  30787  nmooval  30795  nmooge0  30799  nmoub3i  30805  bloln  30816  nmblore  30818  hosval  31772  homval  31773  hodval  31774  hfsval  31775  hfmval  31776  homulass  31834  hoadddir  31836  nmopub2tALT  31941  nmfnleub2  31958  kbval  31986  lnopmul  31999  0lnfn  32017  lnopcoi  32035  nmcoplb  32062  nmcfnlb  32086  kbass2  32149  nmopleid  32171  hstoh  32264  mdi  32327  dmdi  32334  dmdi4  32339  fdifsuppconst  32701  supxrnemnf  32775  rloccring  33242  reofld  33337  nsgmgclem  33404  rhmimaidl  33425  dfufd2lem  33542  r1plmhm  33595  r1pquslmic  33596  lbsdiflsp0  33639  evls1fldgencl  33680  zarclsun  33816  zarclsint  33818  bnj605  34883  bnj607  34892  bnj1097  34957  fnrelpredd  35065  cusgredgex  35089  topdifinffinlem  37313  lindsdom  37574  lindsenlbs  37575  ftc1anclem2  37654  fzmul  37701  nninfnub  37711  exidreslem  37837  grposnOLD  37842  ghomf  37850  rngohomf  37926  rngohom1  37928  rngohomadd  37929  rngohommul  37930  rngoiso1o  37939  rngoisohom  37940  igenmin  38024  lkrcl  39048  lkrf0  39049  omlfh1N  39214  tendoex  40932  uzindd  41933  primrootsunit1  42054  sticksstones3  42105  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  sticksstones17  42120  3anrabdioph  42738  3orrabdioph  42739  rencldnfilem  42776  dvdsabsmod0  42944  jm2.18  42945  jm2.25  42956  jm2.15nn0  42960  tfsconcatlem  43298  onsucunitp  43335  addrfv  44438  subrfv  44439  mulvfv  44440  bi3impa  44455  ssfiunibd  45224  supminfxr  45379  limsupgtlem  45698  xlimmnfv  45755  xlimpnfv  45759  dvnmul  45864  stoweidlem34  45955  stoweidlem48  45969  sge0cl  46302  sge0xp  46350  ovnsubaddlem1  46491  aovmpt4g  47116  gboge9  47638