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  1346  3impdir  1351  syl3an9b  1435  biimp3a  1470  stoic3  1775  rspec3  3260  vtocl3gaf  3558  vtocl3ga  3560  rspc3v  3615  raltpg  4672  rextpg  4673  disjiun  5105  otthg  5458  3optocl  5749  fun2ssres  6578  funtpg  6588  funssfv  6894  f1elima  7252  ot1stg  7997  ot2ndg  7998  smogt  8376  omord2  8574  omword  8577  oeword  8597  omabslem  8657  ecovass  8833  fpmg  8877  findcard  9172  endjudisj  10176  cfsmolem  10277  ingru  10822  addasspi  10902  mulasspi  10904  ltapi  10910  ltmpi  10911  axpre-ltadd  11174  leltne  11317  dedekind  11391  recextlem2  11861  divdiv32  11942  divdiv1  11945  lble  12187  fnn0ind  12685  supminf  12944  xrleltne  13154  xrmaxeq  13188  xrmineq  13189  iccgelb  13410  elicc4  13421  iccsplit  13492  elfz  13520  modabs  13911  expgt0  14103  expge0  14106  expge1  14107  mulexpz  14110  expp1z  14119  expm1  14120  expmordi  14175  digit1  14245  faclbnd4  14305  faclbnd5  14306  ccatsymb  14589  s3eqs2s1eq  14946  abssubne0  15324  binom  15835  dvds0lem  16273  dvdsnegb  16280  muldvds1  16287  muldvds2  16288  dvdscmulr  16291  dvdsmulcr  16292  divalgmodcl  16413  gcd2n0cl  16515  gcdaddm  16531  lcmdvds  16614  prmdvdsexp  16721  rpexp1i  16729  monpropd  17737  prfval  18198  xpcpropd  18207  curf2ndf  18246  eqglact  19149  ghmqusker  19257  mndodcongi  19511  oddvdsnn0  19512  efgi0  19688  efgi1  19689  efgsval2  19701  lss0cl  20891  mpofrlmd  21724  evls1fpws  22294  scmatscmid  22431  pmatcollpw3fi1lem1  22711  cnpval  23161  cnf2  23174  cnnei  23207  lfinun  23450  ptpjcn  23536  cnmptk2  23611  flfval  23915  cnmpt2plusg  24013  cnmpt2vsca  24120  ustincl  24133  xbln0  24340  blssec  24361  blpnfctr  24362  mopni2  24419  mopni3  24420  nmoval  24641  nmocl  24646  isnghm2  24650  isnmhm2  24678  cnmpt2ds  24770  metdseq0  24781  cnmpt2ip  25187  caucfil  25222  mbfimasn  25572  dvnf  25868  dvnbss  25869  coemul  26196  dvply1  26230  dvnply2  26234  pserdvlem2  26377  logeftb  26530  advlogexp  26602  cxpne0  26624  cxpp1  26627  elno2  27604  f1otrg  28784  ax5seglem9  28850  uhgrn0  28980  upgrn0  29002  upgrle  29003  uhgrwkspthlem2  29670  frgrhash2wsp  30247  sspval  30638  sspnval  30652  lnof  30670  nmooval  30678  nmooge0  30682  nmoub3i  30688  bloln  30699  nmblore  30701  hosval  31655  homval  31656  hodval  31657  hfsval  31658  hfmval  31659  homulass  31717  hoadddir  31719  nmopub2tALT  31824  nmfnleub2  31841  kbval  31869  lnopmul  31882  0lnfn  31900  lnopcoi  31918  nmcoplb  31945  nmcfnlb  31969  kbass2  32032  nmopleid  32054  hstoh  32147  mdi  32210  dmdi  32217  dmdi4  32222  tpssg  32452  fdifsuppconst  32600  supxrnemnf  32682  elrgspnlem2  33175  rloccring  33202  reofld  33296  nsgmgclem  33363  rhmimaidl  33384  dfufd2lem  33501  r1plmhm  33554  r1pquslmic  33555  lbsdiflsp0  33601  evls1fldgencl  33646  zarclsun  33830  zarclsint  33832  bnj605  34867  bnj607  34876  bnj1097  34941  fnrelpredd  35049  cusgredgex  35073  topdifinffinlem  37294  lindsdom  37567  lindsenlbs  37568  ftc1anclem2  37647  fzmul  37694  nninfnub  37704  exidreslem  37830  grposnOLD  37835  ghomf  37843  rngohomf  37919  rngohom1  37921  rngohomadd  37922  rngohommul  37923  rngoiso1o  37932  rngoisohom  37933  igenmin  38017  lkrcl  39039  lkrf0  39040  omlfh1N  39205  tendoex  40923  uzindd  41919  primrootsunit1  42039  sticksstones3  42090  sticksstones10  42097  sticksstones12a  42099  sticksstones12  42100  sticksstones17  42105  3anrabdioph  42737  3orrabdioph  42738  rencldnfilem  42775  dvdsabsmod0  42943  jm2.18  42944  jm2.25  42955  jm2.15nn0  42959  tfsconcatlem  43292  onsucunitp  43329  addrfv  44426  subrfv  44427  mulvfv  44428  bi3impa  44443  ssfiunibd  45272  supminfxr  45425  limsupgtlem  45742  xlimmnfv  45799  xlimpnfv  45803  dvnmul  45908  stoweidlem34  45999  stoweidlem48  46013  sge0cl  46346  sge0xp  46394  ovnsubaddlem1  46535  aovmpt4g  47166  gboge9  47704