Theorem ad2ant2l 743

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 713	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantll 711	1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396

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-an 397

This theorem is referenced by:  funcnvqp  6505  mpteqb  6903  mpofunOLD  7408  soxp  7979  wfrlem4OLD  8152  oaass  8401  undifixp  8731  undomOLD  8856  xpdom2  8863  tcrank  9651  inawinalem  10454  addcanpr  10811  ltsosr  10859  1re  10984  add42  11205  muladd  11416  mulsub  11427  divmuleq  11689  ltmul12a  11840  lemul12b  11841  lemul12a  11842  mulge0b  11854  qaddcl  12714  qmulcl  12716  iooshf  13167  fzass4  13303  elfzomelpfzo  13500  modid  13625  swrdccatin2  14451  pfxccatin12  14455  cshwleneq  14539  s2eq2seq  14659  tanaddlem  15884  fpwipodrs  18267  gsumsgrpccat  18487  issubg4  18783  ghmpreima  18865  cntzsubg  18952  symgfixf1  19054  islmodd  20138  lssvsubcl  20214  lssvscl  20226  lmhmf1o  20317  pwsdiaglmhm  20328  lmimco  21060  scmatghm  21691  scmatmhm  21692  mat2pmatscmxcl  21898  fctop  22163  cctop  22165  opnneissb  22274  pnrmopn  22503  hausnei2  22513  neitx  22767  txcnmpt  22784  txrest  22791  tx1stc  22810  fbssfi  22997  opnfbas  23002  rnelfmlem  23112  alexsubALTlem3  23209  metcnp3  23705  cncfmet  24081  evth  24131  caucfil  24456  ovolun  24672  dveflem  25152  efnnfsumcl  26261  efchtdvds  26317  lgsdir2  26487  axdimuniq  27290  axcontlem2  27342  clwwlkf1  28422  frgrwopreglem5lem  28693  frgrwopreglem5ALT  28695  friendship  28772  hvsub4  29408  his35  29459  shscli  29688  5oalem2  30026  3oalem2  30034  hosub4  30184  hmops  30391  hmopm  30392  hmopco  30394  adjmul  30463  adjadd  30464  mdslmd1lem1  30696  mdslmd1lem2  30697  satffunlem  33372  elmrsubrn  33491  dfon2lem6  33773  funline  34453  neibastop2lem  34558  isbasisrelowllem1  35535  isbasisrelowllem2  35536  mbfposadd  35833  itg2addnc  35840  fdc  35912  seqpo  35914  ismtyval  35967  paddss12  37840  mzpcompact2lem  40580  jm2.26  40831  fmtnofac2lem  45031  rnghmsubcsetclem2  45545  rhmsubcsetclem2  45591  rhmsubcrngclem2  45597  zlmodzxzsubm  45706  ltsubaddb  45866  ltsubsubb  45867