Theorem adantrd 495

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 486	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2		adantrd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 34	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 209  df-an 400

This theorem is referenced by:  im2anan9  629  jaoa  968  prlem1  1066  cad0  1638  dfsb1  2512  unineq  4240  dfopif  4828  elssabg  5299  exopxfr2  5816  tz7.7  6372  oneqmini  6399  fvun1  6958  fconst5  7190  fpropnf1  7251  f1ounsn  7256  isomin  7321  isofrlem  7324  poxp  8108  poseq  8138  tposfo2  8229  onfununi  8312  tfrlem9a  8357  oecl  8506  oawordri  8519  omwordri  8541  odi  8548  pssnn  9137  prdom2  9962  acni2  10002  cardinfima  10053  cfslb2n  10225  infpssrlem4  10263  axdc3lem4  10410  brdom6disj  10489  tskr1om  10725  indpi  10865  1idpr  10987  1re  11181  mulge0  11705  infm3  12151  uzind  12665  suprfinzcl  12687  uzwo  12912  xrlttr  13142  xmullem2  13268  snunico  13483  fzen  13546  fz0fzelfz0  13639  sqlecan  14222  hashf1lem2  14469  ccatsymb  14596  lo1le  15679  fsumss  15752  ntrivcvgfvn0  15929  fprodss  15978  smupvallem  16517  zeqzmulgcd  16544  lcmgcdlem  16640  lcmdvds  16642  lcmfunsnlem2lem1  16672  coprmproddvdslem  16696  cncongr2  16702  exprmfct  16739  infpnlem1  16946  prmdvdsprmop  17079  prmgaplem7  17093  prmlem0  17141  sscfn2  17851  isssc  17853  iszeroi  18042  funcsetcestrclem8  18194  dirge  18635  efgval  19757  dmdprd  20040  dprdw  20052  rhmsubclem4  20734  lpigen  21402  psrbaglefi  21975  matvscl  22488  scmatghm  22590  slesolinv  22737  cpmatacl  22773  pnfnei  23277  mnfnei  23278  cmpcld  23459  isfildlem  23914  metrest  24581  blval2  24619  iscmet3lem2  25351  ivthlem3  25512  mbfi1fseqlem4  25777  itg2seq  25801  aalioulem6  26398  taylthlem2  26434  chpchtsum  27280  dchrmulcl  27310  bcmono  27338  nosupno  27764  nosupbday  27766  noinfno  27779  noinfbday  27781  nocvxminlem  27844  cuteq1  27907  oncutlt  28354  oniso  28361  bdayn0p1  28459  bdayfinbndlem2  28558  z12sge0  28573  cgrg3col4  29044  brbtwn2  29103  axeuclid  29161  umgredg  29336  pthdivtx  29924  pthdlem1  29963  shsvs  31523  cnlnssadj  32280  atexch  32581  mdsymlem5  32607  disjxpin  32785  fldextrspunlsplem  33967  sigaclci  34426  fnrelpredd  35384  satfv0  35705  satffunlem2lem1  35751  dmopab3rexdif  35752  elfuns  36260  altopth1  36312  btwnexch2  36370  ifscgr  36391  colinbtwnle  36465  trer  36673  elicc3  36674  bj-imdirval3  37673  bj-finsumval0  37774  difunieq  37865  fvineqsneu  37902  fvineqsneq  37903  poimirlem27  38143  poimir  38149  cnambfre  38164  itg2addnclem2  38168  itg2addnc  38170  areacirclem1  38204  heiborlem4  38310  elghomlem2OLD  38382  rngo2  38403  ispridl2  38534  ispridlc  38566  iss2  38840  membpartlem19  39410  paddasslem14  40454  ispsubcl2N  40568  cdleme29ex  40995  cdlemefr29exN  41023  eldiophss  43352  rencldnfilem  43394  oaabsb  43868  cantnfresb  43898  tfsconcatrn  43916  naddwordnexlem1  43971  clsk1indlem3  44616  ntrneikb  44667  mnuop3d  44844  ax6e2ndeq  45132  suctrALT2  45409  relpmin  45525  relpfrlem  45526  2reu3  47701  iccpartiltu  48025  bgoldbtbndlem2  48425  grtrimap  48567  grimgrtri  48568  isubgr3stgrlem6  48590  isubgr3stgr  48594  pgnbgreunbgrlem1  48732  pgnbgreunbgrlem4  48738  itschlc0xyqsol1  49385  resipos  49593  elsetrecslem  50317  aacllem  50419