Theorem anim2d 613

Description: Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 14-May-1993.)

Hypothesis

Ref	Expression
anim1d.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
anim2d	⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒)))

Proof of Theorem anim2d

Step	Hyp	Ref	Expression
1		idd 24	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
2		anim1d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	anim12d 610	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  darii  2661  festino  2670  baroco  2672  moeq3  3709  sbcimdv  3852  ssel  3976  sselOLD  3977  sscon  4139  uniss  4917  trel3  5276  ssopab2  5547  coss1  5856  fununi  6624  imadif  6633  fss  6735  ssimaex  6977  ssoprab2  7477  poxp  8114  soxp  8115  poseq  8144  suppofssd  8188  pmss12g  8863  ss2ixp  8904  xpdom2  9067  fisup2g  9463  fisupcl  9464  fiinf2g  9495  inf3lem1  9623  epfrs  9726  cfub  10244  cflm  10245  fin23lem34  10341  isf32lem2  10349  axcc4  10434  domtriomlem  10437  ltexprlem3  11033  nnunb  12468  indstr  12900  qbtwnxr  13179  qsqueeze  13180  xrsupsslem  13286  xrinfmsslem  13287  ioc0  13371  climshftlem  15518  o1rlimmul  15563  ramub2  16947  monmat2matmon  22326  tgcl  22472  neips  22617  ssnei2  22620  tgcnp  22757  cnpnei  22768  cnpco  22771  hauscmplem  22910  hauscmp  22911  llyss  22983  nllyss  22984  lfinun  23029  kgen2ss  23059  txcnpi  23112  txcmplem1  23145  fgss  23377  cnpflf2  23504  fclsss1  23526  fclscf  23529  alexsubALT  23555  cnextcn  23571  tsmsxp  23659  mopni3  24003  psmetutop  24076  tngngp3  24173  iscau4  24796  caussi  24814  ovolgelb  24997  mbfi1flim  25241  ellimc3  25396  lhop1  25531  tgbtwndiff  27788  axcontlem4  28256  clwwlknonwwlknonb  29390  sspmval  30017  shmodsi  30673  atcvat4i  31681  cdj3lem2b  31721  ifeqeqx  31805  acunirnmpt  31915  xrge0infss  32004  crefss  32860  issgon  33152  cvmlift2lem12  34336  satfv1  34385  satfvsucsuc  34387  ss2mcls  34590  btwndiff  35030  seglecgr12im  35113  fnessref  35290  waj-ax  35347  lukshef-ax2  35348  bj-isrvec  36223  icorempo  36280  finxpreclem1  36318  fvineqsneq  36341  pibt2  36346  tan2h  36528  poimirlem31  36567  poimir  36569  mblfinlem3  36575  mblfinlem4  36576  ismblfin  36577  cvrat4  38362  athgt  38375  ps-2  38397  paddss1  38736  paddss2  38737  cdlemg33b0  39620  cdlemg33a  39625  dihjat1lem  40347  fphpdo  41603  irrapxlem2  41609  pell14qrss1234  41642  pell1qrss14  41654  acongtr  41765  ofoaid1  42156  ofoaid2  42157  fzunt  42254  fzuntd  42255  fzunt1d  42256  fzuntgd  42257  grumnudlem  43092  ax6e2eq  43366  islptre  44383  limccog  44384  opnneilv  47589