Theorem ad2ant2l 797

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)

Hypothesis

Ref	Expression
ad2ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad2ant2l	⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒)

Proof of Theorem ad2ant2l

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantrl 752	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantll 750	1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  funcnvqp  5990  mpteqb  6338  mpt2fun  6804  soxp  7335  wfrlem4  7463  oaass  7686  undifixp  7986  undom  8089  xpdom2  8096  tcrank  8785  inawinalem  9549  addcanpr  9906  ltsosr  9953  1re  10077  add42  10295  muladd  10500  mulsub  10511  divmuleq  10768  ltmul12a  10917  lemul12b  10918  lemul12a  10919  mulge0b  10931  qaddcl  11842  qmulcl  11844  iooshf  12290  fzass4  12417  elfzomelpfzo  12612  modid  12735  cshwleneq  13609  s2eq2seq  13728  tanaddlem  14940  fpwipodrs  17211  issubg4  17660  ghmpreima  17729  cntzsubg  17815  symgfixf1  17903  islmodd  18917  lssvsubcl  18992  lssvscl  19003  lmhmf1o  19094  pwsdiaglmhm  19105  lmimco  20231  scmatghm  20387  scmatmhm  20388  mat2pmatscmxcl  20593  fctop  20856  cctop  20858  opnneissb  20966  pnrmopn  21195  hausnei2  21205  neitx  21458  txcnmpt  21475  txrest  21482  tx1stc  21501  fbssfi  21688  opnfbas  21693  rnelfmlem  21803  alexsubALTlem3  21900  metcnp3  22392  cncfmet  22758  evth  22805  caucfil  23127  ovolun  23313  dveflem  23787  efnnfsumcl  24874  efchtdvds  24930  lgsdir2  25100  axdimuniq  25838  axcontlem2  25890  frgrwopreglem5lem  27300  frgrwopreglem5ALT  27302  friendship  27386  hvsub4  28022  his35  28073  shscli  28304  5oalem2  28642  3oalem2  28650  hosub4  28800  hmops  29007  hmopm  29008  hmopco  29010  adjmul  29079  adjadd  29080  mdslmd1lem1  29312  mdslmd1lem2  29313  elmrsubrn  31543  dfon2lem6  31817  funline  32374  neibastop2lem  32480  isbasisrelowllem1  33333  isbasisrelowllem2  33334  mbfposadd  33587  itg2addnc  33594  fdc  33671  seqpo  33673  ismtyval  33729  paddss12  35423  mzpcompact2lem  37631  jm2.26  37886  fmtnofac2lem  41805  rnghmsubcsetclem2  42301  rhmsubcsetclem2  42347  rhmsubcrngclem2  42353  zlmodzxzsubm  42462  ltsubaddb  42629  ltsubsubb  42630