Theorem adantrd 491

Description: Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.)

Hypothesis

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

Assertion

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

Proof of Theorem adantrd

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2		adantrd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 34	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 207  df-an 396

This theorem is referenced by:  im2anan9  620  jaoa  957  prlem1  1054  cad0  1619  dfsb1  2485  unineq  4240  dfopif  4826  elssabg  5288  exopxfr2  5793  tz7.7  6343  oneqmini  6370  fvun1  6925  fconst5  7152  fpropnf1  7213  f1ounsn  7218  isomin  7283  isofrlem  7286  poxp  8070  poseq  8100  tposfo2  8191  onfununi  8273  tfrlem9a  8317  oecl  8464  oawordri  8477  omwordri  8499  odi  8506  pssnn  9093  prdom2  9916  acni2  9956  cardinfima  10007  cfslb2n  10178  infpssrlem4  10216  axdc3lem4  10363  brdom6disj  10442  tskr1om  10678  indpi  10818  1idpr  10940  1re  11132  mulge0  11655  infm3  12101  uzind  12584  suprfinzcl  12606  uzwo  12824  xrlttr  13054  xmullem2  13180  snunico  13395  fzen  13457  fz0fzelfz0  13550  sqlecan  14132  hashf1lem2  14379  ccatsymb  14506  lo1le  15575  fsumss  15648  ntrivcvgfvn0  15822  fprodss  15871  smupvallem  16410  zeqzmulgcd  16437  lcmgcdlem  16533  lcmdvds  16535  lcmfunsnlem2lem1  16565  coprmproddvdslem  16589  cncongr2  16595  exprmfct  16631  infpnlem1  16838  prmdvdsprmop  16971  prmgaplem7  16985  prmlem0  17033  sscfn2  17742  isssc  17744  iszeroi  17933  funcsetcestrclem8  18085  dirge  18526  efgval  19646  dmdprd  19929  dprdw  19941  rhmsubclem4  20621  lpigen  21290  psrbaglefi  21882  matvscl  22375  scmatghm  22477  slesolinv  22624  cpmatacl  22660  pnfnei  23164  mnfnei  23165  cmpcld  23346  isfildlem  23801  metrest  24468  blval2  24506  iscmet3lem2  25248  ivthlem3  25410  mbfi1fseqlem4  25675  itg2seq  25699  aalioulem6  26301  taylthlem2  26338  chpchtsum  27186  dchrmulcl  27216  bcmono  27244  nosupno  27671  nosupbday  27673  noinfno  27686  noinfbday  27688  nocvxminlem  27750  cuteq1  27813  oncutlt  28260  oniso  28267  bdayn0p1  28365  bdayfinbndlem2  28464  z12sge0  28479  cgrg3col4  28925  brbtwn2  28978  axeuclid  29036  umgredg  29211  pthdivtx  29800  pthdlem1  29839  shsvs  31398  cnlnssadj  32155  atexch  32456  mdsymlem5  32482  disjxpin  32663  fldextrspunlsplem  33830  sigaclci  34289  fnrelpredd  35247  satfv0  35552  satffunlem2lem1  35598  dmopab3rexdif  35599  elfuns  36107  altopth1  36159  btwnexch2  36217  ifscgr  36238  colinbtwnle  36312  trer  36510  elicc3  36511  bj-imdirval3  37389  bj-finsumval0  37490  difunieq  37579  fvineqsneu  37616  fvineqsneq  37617  poimirlem27  37848  poimir  37854  cnambfre  37869  itg2addnclem2  37873  itg2addnc  37875  areacirclem1  37909  heiborlem4  38015  elghomlem2OLD  38087  rngo2  38108  ispridl2  38239  ispridlc  38271  iss2  38537  membpartlem19  39070  paddasslem14  40093  ispsubcl2N  40207  cdleme29ex  40634  cdlemefr29exN  40662  eldiophss  43016  rencldnfilem  43062  oaabsb  43536  cantnfresb  43566  tfsconcatrn  43584  naddwordnexlem1  43639  clsk1indlem3  44284  ntrneikb  44335  mnuop3d  44512  ax6e2ndeq  44800  suctrALT2  45077  relpmin  45193  relpfrlem  45194  2reu3  47356  iccpartiltu  47668  bgoldbtbndlem2  48052  grtrimap  48194  grimgrtri  48195  isubgr3stgrlem6  48217  isubgr3stgr  48221  pgnbgreunbgrlem1  48359  pgnbgreunbgrlem4  48365  itschlc0xyqsol1  49012  resipos  49220  elsetrecslem  49944  aacllem  50046