Theorem 3impa 1111

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 1090

This theorem is referenced by:  3imp  1112  3adant1  1131  3adant2  1132  ex3  1347  3impdir  1352  syl3an9b  1435  biimp3a  1470  stoic3  1779  rspec3  3278  rspc3v  3627  raltpg  4702  rextpg  4703  disjiun  5135  otthg  5485  3optocl  5771  fun2ssres  6591  funtpg  6601  funssfv  6910  f1elima  7259  ot1stg  7986  ot2ndg  7987  smogt  8364  omord2  8564  omword  8567  oeword  8587  omabslem  8646  ecovass  8815  fpmg  8859  findcard  9160  endjudisj  10160  cfsmolem  10262  ingru  10807  addasspi  10887  mulasspi  10889  ltapi  10895  ltmpi  10896  axpre-ltadd  11159  leltne  11300  dedekind  11374  recextlem2  11842  divdiv32  11919  divdiv1  11922  lble  12163  fnn0ind  12658  supminf  12916  xrleltne  13121  xrmaxeq  13155  xrmineq  13156  iccgelb  13377  elicc4  13388  iccsplit  13459  elfz  13487  modabs  13866  expgt0  14058  expge0  14061  expge1  14062  mulexpz  14065  expp1z  14074  expm1  14075  expmordi  14129  digit1  14197  faclbnd4  14254  faclbnd5  14255  ccatsymb  14529  s3eqs2s1eq  14886  abssubne0  15260  binom  15773  dvds0lem  16207  dvdsnegb  16214  muldvds1  16221  muldvds2  16222  dvdscmulr  16225  dvdsmulcr  16226  divalgmodcl  16347  gcd2n0cl  16447  gcdaddm  16463  lcmdvds  16542  prmdvdsexp  16649  rpexp1i  16657  monpropd  17681  prfval  18148  xpcpropd  18158  curf2ndf  18197  eqglact  19054  mndodcongi  19406  oddvdsnn0  19407  efgi0  19583  efgi1  19584  efgsval2  19596  lss0cl  20550  mpofrlmd  21324  scmatscmid  22000  pmatcollpw3fi1lem1  22280  cnpval  22732  cnf2  22745  cnnei  22778  lfinun  23021  ptpjcn  23107  cnmptk2  23182  flfval  23486  cnmpt2plusg  23584  cnmpt2vsca  23691  ustincl  23704  xbln0  23912  blssec  23933  blpnfctr  23934  mopni2  23994  mopni3  23995  nmoval  24224  nmocl  24229  isnghm2  24233  isnmhm2  24261  cnmpt2ds  24351  metdseq0  24362  cnmpt2ip  24757  caucfil  24792  mbfimasn  25141  dvnf  25436  dvnbss  25437  coemul  25758  dvply1  25789  dvnply2  25792  pserdvlem2  25932  logeftb  26084  advlogexp  26155  cxpne0  26177  cxpp1  26180  elno2  27147  f1otrg  28112  ax5seglem9  28185  uhgrn0  28317  upgrn0  28339  upgrle  28340  uhgrwkspthlem2  29001  frgrhash2wsp  29575  sspval  29964  sspnval  29978  lnof  29996  nmooval  30004  nmooge0  30008  nmoub3i  30014  bloln  30025  nmblore  30027  hosval  30981  homval  30982  hodval  30983  hfsval  30984  hfmval  30985  homulass  31043  hoadddir  31045  nmopub2tALT  31150  nmfnleub2  31167  kbval  31195  lnopmul  31208  0lnfn  31226  lnopcoi  31244  nmcoplb  31271  nmcfnlb  31295  kbass2  31358  nmopleid  31380  hstoh  31473  mdi  31536  dmdi  31543  dmdi4  31548  fdifsuppconst  31899  supxrnemnf  31969  reofld  32448  nsgmgclem  32511  ghmqusker  32521  rhmimaidl  32539  evls1fpws  32635  lbsdiflsp0  32700  zarclsun  32839  zarclsint  32841  bnj605  33907  bnj607  33916  bnj1097  33981  fnrelpredd  34081  cusgredgex  34101  topdifinffinlem  36217  lindsdom  36471  lindsenlbs  36472  ftc1anclem2  36551  fzmul  36598  nninfnub  36608  exidreslem  36734  grposnOLD  36739  ghomf  36747  rngohomf  36823  rngohom1  36825  rngohomadd  36826  rngohommul  36827  rngoiso1o  36836  rngoisohom  36837  igenmin  36921  lkrcl  37951  lkrf0  37952  omlfh1N  38117  tendoex  39835  uzindd  40831  sticksstones3  40953  sticksstones10  40960  sticksstones12a  40962  sticksstones12  40963  sticksstones17  40968  3anrabdioph  41506  3orrabdioph  41507  rencldnfilem  41544  dvdsabsmod0  41712  jm2.18  41713  jm2.25  41724  jm2.15nn0  41728  tfsconcatlem  42072  onsucunitp  42109  addrfv  43214  subrfv  43215  mulvfv  43216  bi3impa  43231  ssfiunibd  44006  supminfxr  44161  limsupgtlem  44480  xlimmnfv  44537  xlimpnfv  44541  dvnmul  44646  stoweidlem34  44737  stoweidlem48  44751  sge0cl  45084  sge0xp  45132  ovnsubaddlem1  45273  aovmpt4g  45896  gboge9  46419