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 395

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 396

This theorem is referenced by:  funcnvqp  6612  mpteqb  7017  mpofunOLD  7536  soxp  8118  wfrlem4OLD  8315  oaass  8564  nadd42  8701  naddel12  8702  undifixp  8931  undomOLD  9063  xpdom2  9070  tcrank  9882  inawinalem  10687  addcanpr  11044  ltsosr  11092  1re  11219  add42  11440  muladd  11651  mulsub  11662  divmuleq  11924  ltmul12a  12075  lemul12b  12076  lemul12a  12077  mulge0b  12089  qaddcl  12954  qmulcl  12956  iooshf  13408  fzass4  13544  elfzomelpfzo  13741  modid  13866  swrdccatin2  14684  pfxccatin12  14688  cshwleneq  14772  s2eq2seq  14893  tanaddlem  16114  fpwipodrs  18498  gsumsgrpccat  18758  issubg4  19062  ghmpreima  19153  cntzsubg  19245  symgfixf1  19347  islmodd  20621  lssvsubcl  20699  lssvscl  20711  lmhmf1o  20802  pwsdiaglmhm  20813  lmimco  21619  scmatghm  22256  scmatmhm  22257  mat2pmatscmxcl  22463  fctop  22728  cctop  22730  opnneissb  22839  pnrmopn  23068  hausnei2  23078  neitx  23332  txcnmpt  23349  txrest  23356  tx1stc  23375  fbssfi  23562  opnfbas  23567  rnelfmlem  23677  alexsubALTlem3  23774  metcnp3  24270  cncfmet  24650  evth  24706  caucfil  25032  ovolun  25249  dveflem  25732  efnnfsumcl  26844  efchtdvds  26900  lgsdir2  27070  precsexlem11  27903  axdimuniq  28439  axcontlem2  28491  clwwlkf1  29570  frgrwopreglem5lem  29841  frgrwopreglem5ALT  29843  friendship  29920  hvsub4  30558  his35  30609  shscli  30838  5oalem2  31176  3oalem2  31184  hosub4  31334  hmops  31541  hmopm  31542  hmopco  31544  adjmul  31613  adjadd  31614  mdslmd1lem1  31846  mdslmd1lem2  31847  satffunlem  34691  elmrsubrn  34810  dfon2lem6  35065  funline  35419  neibastop2lem  35549  isbasisrelowllem1  36540  isbasisrelowllem2  36541  mbfposadd  36839  itg2addnc  36846  fdc  36917  seqpo  36919  ismtyval  36972  paddss12  38994  zaddcom  41628  zmulcom  41632  mzpcompact2lem  41792  jm2.26  42044  orddif0suc  42321  tfsconcatun  42390  oaun3lem2  42428  fmtnofac2lem  46535  rnghmsubcsetclem2  46963  rhmsubcsetclem2  47009  rhmsubcrngclem2  47015  zlmodzxzsubm  47124  ltsubaddb  47283  ltsubsubb  47284