Theorem 3impa 1106

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-3an 1085

This theorem is referenced by:  3imp  1107  3adant1  1126  3adant2  1127  ex3  1342  3impdir  1347  syl3an9b  1430  biimp3a  1465  stoic3  1777  rspec3  3214  rspc3v  3638  raltpg  4636  rextpg  4637  disjiun  5055  otthg  5379  3optocl  5649  fun2ssres  6401  funtpg  6411  funssfv  6693  f1elima  7023  ot1stg  7705  ot2ndg  7706  smogt  8006  omord2  8195  omword  8198  oeword  8218  omabslem  8275  ecovass  8406  fpmg  8434  findcard  8759  endjudisj  9596  cfsmolem  9694  ingru  10239  addasspi  10319  mulasspi  10321  ltapi  10327  ltmpi  10328  axpre-ltadd  10591  leltne  10732  dedekind  10805  recextlem2  11273  divdiv32  11350  divdiv1  11353  lble  11595  fnn0ind  12084  supminf  12338  xrleltne  12541  xrmaxeq  12575  xrmineq  12576  iccgelb  12796  elicc4  12806  iccsplit  12874  elfz  12901  modabs  13275  expgt0  13465  expge0  13468  expge1  13469  mulexpz  13472  expp1z  13481  expm1  13482  expmordi  13534  digit1  13601  faclbnd4  13660  faclbnd5  13661  ccatsymb  13938  s3eqs2s1eq  14302  abssubne0  14678  binom  15187  dvds0lem  15622  dvdsnegb  15629  muldvds1  15636  muldvds2  15637  dvdscmulr  15640  dvdsmulcr  15641  divalgmodcl  15760  gcd2n0cl  15860  gcdaddm  15875  lcmdvds  15954  prmdvdsexp  16061  rpexp1i  16067  monpropd  17009  prfval  17451  xpcpropd  17460  curf2ndf  17499  eqglact  18333  mndodcongi  18673  oddvdsnn0  18674  efgi0  18848  efgi1  18849  efgsval2  18861  lss0cl  19720  mpofrlmd  20923  scmatscmid  21117  pmatcollpw3fi1lem1  21396  cnpval  21846  cnf2  21859  cnnei  21892  lfinun  22135  ptpjcn  22221  cnmptk2  22296  flfval  22600  cnmpt2plusg  22698  cnmpt2vsca  22805  ustincl  22818  xbln0  23026  blssec  23047  blpnfctr  23048  mopni2  23105  mopni3  23106  nmoval  23326  nmocl  23331  isnghm2  23335  isnmhm2  23363  cnmpt2ds  23453  metdseq0  23464  cnmpt2ip  23853  caucfil  23888  mbfimasn  24235  dvnf  24526  dvnbss  24527  coemul  24844  dvply1  24875  dvnply2  24878  pserdvlem2  25018  logeftb  25169  advlogexp  25240  cxpne0  25262  cxpp1  25265  f1otrg  26659  ax5seglem9  26725  uhgrn0  26854  upgrn0  26876  upgrle  26877  uhgrwkspthlem2  27537  frgrhash2wsp  28113  sspval  28502  sspnval  28516  lnof  28534  nmooval  28542  nmooge0  28546  nmoub3i  28552  bloln  28563  nmblore  28565  hosval  29519  homval  29520  hodval  29521  hfsval  29522  hfmval  29523  homulass  29581  hoadddir  29583  nmopub2tALT  29688  nmfnleub2  29705  kbval  29733  lnopmul  29746  0lnfn  29764  lnopcoi  29782  nmcoplb  29809  nmcfnlb  29833  kbass2  29896  nmopleid  29918  hstoh  30011  mdi  30074  dmdi  30081  dmdi4  30086  supxrnemnf  30495  reofld  30915  lbsdiflsp0  31024  bnj605  32181  bnj607  32190  bnj1097  32255  cusgredgex  32370  elno2  33163  topdifinffinlem  34630  lindsdom  34888  lindsenlbs  34889  ftc1anclem2  34970  fzmul  35018  nninfnub  35028  exidreslem  35157  grposnOLD  35162  ghomf  35170  rngohomf  35246  rngohom1  35248  rngohomadd  35249  rngohommul  35250  rngoiso1o  35259  rngoisohom  35260  igenmin  35344  lkrcl  36230  lkrf0  36231  omlfh1N  36396  tendoex  38113  3anrabdioph  39386  3orrabdioph  39387  rencldnfilem  39424  dvdsabsmod0  39591  jm2.18  39592  jm2.25  39603  jm2.15nn0  39607  addrfv  40808  subrfv  40809  mulvfv  40810  bi3impa  40825  ssfiunibd  41583  supminfxr  41747  limsupgtlem  42065  xlimmnfv  42122  xlimpnfv  42126  dvnmul  42235  stoweidlem34  42326  stoweidlem48  42340  sge0cl  42670  sge0xp  42718  ovnsubaddlem1  42859  aovmpt4g  43407  gboge9  43936