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  1131  3adant2  1132  ex3  1348  3impdir  1353  syl3an9b  1437  biimp3a  1472  stoic3  1778  rspec3  3258  vtocl3gaf  3538  vtocl3ga  3540  rspc3v  3594  raltpg  4657  rextpg  4658  disjiun  5088  otthg  5441  3optocl  5729  fun2ssres  6545  funtpg  6555  funssfv  6863  f1elima  7219  ot1stg  7957  ot2ndg  7958  smogt  8309  omord2  8504  omword  8507  oeword  8528  omabslem  8588  ecovass  8773  fpmg  8818  findcard  9100  endjudisj  10091  cfsmolem  10192  ingru  10738  addasspi  10818  mulasspi  10820  ltapi  10826  ltmpi  10827  axpre-ltadd  11090  leltne  11234  dedekind  11308  recextlem2  11780  divdiv32  11861  divdiv1  11864  lble  12106  fnn0ind  12603  supminf  12860  xrleltne  13071  xrmaxeq  13106  xrmineq  13107  iccgelb  13330  elicc4  13341  iccsplit  13413  elfz  13441  modabs  13836  expgt0  14030  expge0  14033  expge1  14034  mulexpz  14037  expp1z  14046  expm1  14047  expmordi  14102  digit1  14172  faclbnd4  14232  faclbnd5  14233  ccatsymb  14518  s3eqs2s1eq  14873  abssubne0  15252  binom  15765  dvds0lem  16205  dvdsnegb  16212  muldvds1  16219  muldvds2  16220  dvdscmulr  16223  dvdsmulcr  16224  divalgmodcl  16346  gcd2n0cl  16448  gcdaddm  16464  lcmdvds  16547  prmdvdsexp  16654  rpexp1i  16662  monpropd  17673  prfval  18134  xpcpropd  18143  curf2ndf  18182  eqglact  19123  ghmqusker  19231  mndodcongi  19487  oddvdsnn0  19488  efgi0  19664  efgi1  19665  efgsval2  19677  lss0cl  20913  mpofrlmd  21747  evls1fpws  22328  scmatscmid  22465  pmatcollpw3fi1lem1  22745  cnpval  23195  cnf2  23208  cnnei  23241  lfinun  23484  ptpjcn  23570  cnmptk2  23645  flfval  23949  cnmpt2plusg  24047  cnmpt2vsca  24154  ustincl  24167  xbln0  24373  blssec  24394  blpnfctr  24395  mopni2  24452  mopni3  24453  nmoval  24674  nmocl  24679  isnghm2  24683  isnmhm2  24711  cnmpt2ds  24803  metdseq0  24814  cnmpt2ip  25219  caucfil  25254  mbfimasn  25604  dvnf  25900  dvnbss  25901  coemul  26228  dvply1  26262  dvnply2  26266  pserdvlem2  26409  logeftb  26563  advlogexp  26635  cxpne0  26657  cxpp1  26660  elno2  27637  f1otrg  28959  ax5seglem9  29026  uhgrn0  29156  upgrn0  29178  upgrle  29179  uhgrwkspthlem2  29843  frgrhash2wsp  30423  sspval  30815  sspnval  30829  lnof  30847  nmooval  30855  nmooge0  30859  nmoub3i  30865  bloln  30876  nmblore  30878  hosval  31832  homval  31833  hodval  31834  hfsval  31835  hfmval  31836  homulass  31894  hoadddir  31896  nmopub2tALT  32001  nmfnleub2  32018  kbval  32046  lnopmul  32059  0lnfn  32077  lnopcoi  32095  nmcoplb  32122  nmcfnlb  32146  kbass2  32209  nmopleid  32231  hstoh  32324  mdi  32387  dmdi  32394  dmdi4  32399  tpssg  32628  fdifsuppconst  32783  supxrnemnf  32863  elrgspnlem2  33341  rloccring  33368  reofld  33440  nsgmgclem  33508  rhmimaidl  33529  dfufd2lem  33646  r1plmhm  33707  r1pquslmic  33708  lbsdiflsp0  33808  evls1fldgencl  33852  zarclsun  34052  zarclsint  34054  bnj605  35087  bnj607  35096  bnj1097  35161  fnrelpredd  35272  rankfilimb  35283  cusgredgex  35342  topdifinffinlem  37606  lindsdom  37869  lindsenlbs  37870  ftc1anclem2  37949  fzmul  37996  nninfnub  38006  exidreslem  38132  grposnOLD  38137  ghomf  38145  rngohomf  38221  rngohom1  38223  rngohomadd  38224  rngohommul  38225  rngoiso1o  38234  rngoisohom  38235  igenmin  38319  lkrcl  39472  lkrf0  39473  omlfh1N  39638  tendoex  41355  uzindd  42351  primrootsunit1  42471  sticksstones3  42522  sticksstones10  42529  sticksstones12a  42531  sticksstones12  42532  sticksstones17  42537  3anrabdioph  43143  3orrabdioph  43144  rencldnfilem  43181  dvdsabsmod0  43348  jm2.18  43349  jm2.25  43360  jm2.15nn0  43364  tfsconcatlem  43697  onsucunitp  43734  addrfv  44828  subrfv  44829  mulvfv  44830  bi3impa  44845  ssfiunibd  45675  supminfxr  45826  limsupgtlem  46139  xlimmnfv  46196  xlimpnfv  46200  dvnmul  46305  stoweidlem34  46396  stoweidlem48  46410  sge0cl  46743  sge0xp  46791  ovnsubaddlem1  46932  aovmpt4g  47565  gboge9  48128