Theorem anim2d 615

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 612	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:  darii  2665  festino  2674  baroco  2676  moeq3  3614  sbcimdv  3756  ssel  3880  sselOLD  3881  sscon  4039  uniss  4813  trel3  5154  ssopab2  5412  coss1  5709  fununi  6433  imadif  6442  fss  6540  ssimaex  6774  ssoprab2  7257  poxp  7873  soxp  7874  suppofssd  7923  pmss12g  8528  ss2ixp  8569  xpdom2  8718  fisup2g  9062  fisupcl  9063  fiinf2g  9094  inf3lem1  9221  epfrs  9325  cfub  9828  cflm  9829  fin23lem34  9925  isf32lem2  9933  axcc4  10018  domtriomlem  10021  ltexprlem3  10617  nnunb  12051  indstr  12477  qbtwnxr  12755  qsqueeze  12756  xrsupsslem  12862  xrinfmsslem  12863  ioc0  12947  climshftlem  15100  o1rlimmul  15145  ramub2  16530  monmat2matmon  21675  tgcl  21820  neips  21964  ssnei2  21967  tgcnp  22104  cnpnei  22115  cnpco  22118  hauscmplem  22257  hauscmp  22258  llyss  22330  nllyss  22331  lfinun  22376  kgen2ss  22406  txcnpi  22459  txcmplem1  22492  fgss  22724  cnpflf2  22851  fclsss1  22873  fclscf  22876  alexsubALT  22902  cnextcn  22918  tsmsxp  23006  mopni3  23346  psmetutop  23419  tngngp3  23508  iscau4  24130  caussi  24148  ovolgelb  24331  mbfi1flim  24575  ellimc3  24730  lhop1  24865  tgbtwndiff  26551  axcontlem4  27012  clwwlknonwwlknonb  28143  sspmval  28768  shmodsi  29424  atcvat4i  30432  cdj3lem2b  30472  ifeqeqx  30558  acunirnmpt  30670  xrge0infss  30757  crefss  31467  issgon  31757  cvmlift2lem12  32943  satfv1  32992  satfvsucsuc  32994  ss2mcls  33197  poseq  33482  btwndiff  34015  seglecgr12im  34098  fnessref  34232  waj-ax  34289  lukshef-ax2  34290  icorempo  35208  finxpreclem1  35246  fvineqsneq  35269  pibt2  35274  tan2h  35455  poimirlem31  35494  poimir  35496  mblfinlem3  35502  mblfinlem4  35503  ismblfin  35504  cvrat4  37143  athgt  37156  ps-2  37178  paddss1  37517  paddss2  37518  cdlemg33b0  38401  cdlemg33a  38406  dihjat1lem  39128  fphpdo  40283  irrapxlem2  40289  pell14qrss1234  40322  pell1qrss14  40334  acongtr  40444  grumnudlem  41517  ax6e2eq  41791  islptre  42778  limccog  42779  opnneilv  45818