Theorem ad2ant2l 745

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  funcnvqp  6388  mpteqb  6764  mpofun  7255  soxp  7806  wfrlem4  7941  oaass  8170  undifixp  8481  undom  8588  xpdom2  8595  tcrank  9297  inawinalem  10100  addcanpr  10457  ltsosr  10505  1re  10630  add42  10850  muladd  11061  mulsub  11072  divmuleq  11334  ltmul12a  11485  lemul12b  11486  lemul12a  11487  mulge0b  11499  qaddcl  12352  qmulcl  12354  iooshf  12804  fzass4  12940  elfzomelpfzo  13136  modid  13259  swrdccatin2  14082  pfxccatin12  14086  cshwleneq  14170  s2eq2seq  14290  tanaddlem  15511  fpwipodrs  17766  gsumsgrpccat  17996  issubg4  18290  ghmpreima  18372  cntzsubg  18459  symgfixf1  18557  islmodd  19633  lssvsubcl  19708  lssvscl  19720  lmhmf1o  19811  pwsdiaglmhm  19822  lmimco  20533  scmatghm  21138  scmatmhm  21139  mat2pmatscmxcl  21345  fctop  21609  cctop  21611  opnneissb  21719  pnrmopn  21948  hausnei2  21958  neitx  22212  txcnmpt  22229  txrest  22236  tx1stc  22255  fbssfi  22442  opnfbas  22447  rnelfmlem  22557  alexsubALTlem3  22654  metcnp3  23147  cncfmet  23514  evth  23564  caucfil  23887  ovolun  24103  dveflem  24582  efnnfsumcl  25688  efchtdvds  25744  lgsdir2  25914  axdimuniq  26707  axcontlem2  26759  clwwlkf1  27834  frgrwopreglem5lem  28105  frgrwopreglem5ALT  28107  friendship  28184  hvsub4  28820  his35  28871  shscli  29100  5oalem2  29438  3oalem2  29446  hosub4  29596  hmops  29803  hmopm  29804  hmopco  29806  adjmul  29875  adjadd  29876  mdslmd1lem1  30108  mdslmd1lem2  30109  satffunlem  32761  elmrsubrn  32880  dfon2lem6  33146  funline  33716  neibastop2lem  33821  isbasisrelowllem1  34772  isbasisrelowllem2  34773  mbfposadd  35104  itg2addnc  35111  fdc  35183  seqpo  35185  ismtyval  35238  paddss12  37115  mzpcompact2lem  39692  jm2.26  39943  fmtnofac2lem  44085  rnghmsubcsetclem2  44600  rhmsubcsetclem2  44646  rhmsubcrngclem2  44652  zlmodzxzsubm  44761  ltsubaddb  44923  ltsubsubb  44924