Theorem adantrd 497

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 488	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2		adantrd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 35	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  im2anan9  632  jaoa  970  prlem1  1070  cad0  1650  dfsb1  2510  unineq  4232  dfopif  4836  elssabg  5304  exopxfr2  5823  tz7.7  6391  oneqmini  6419  fvun1  6981  fconst5  7216  fpropnf1  7275  f1ounsn  7284  isomin  7349  isofrlem  7352  poxp  8146  poseq  8181  tposfo2  8273  onfununi  8356  tfrlem9a  8401  oecl  8552  oawordri  8565  omwordri  8587  odi  8594  pssnn  9191  prdom2  10092  acni2  10132  cardinfima  10183  cfslb2n  10353  infpssrlem4  10391  axdc3lem4  10538  brdom6disj  10618  tskr1om  10859  indpi  10999  1idpr  11121  1re  11315  mulge0  11841  infm3  12283  uzind  12798  suprfinzcl  12820  uzwo  13045  xrlttr  13276  xmullem2  13402  snunico  13617  fzen  13681  fz0fzelfz0  13775  sqlecan  14360  hashf1lem2  14608  ccatsymb  14735  lo1le  15828  fsumss  15900  ntrivcvgfvn0  16077  fprodss  16124  smupvallem  16662  zeqzmulgcd  16691  lcmgcdlem  16790  lcmdvds  16792  lcmfunsnlem2lem1  16822  coprmproddvdslem  16846  cncongr2  16852  exprmfct  16889  infpnlem1  17097  prmdvdsprmop  17230  prmgaplem7  17244  prmlem0  17292  sscfn2  18002  isssc  18004  iszeroi  18193  funcsetcestrclem8  18345  dirge  18786  efgval  19940  dmdprd  20223  dprdw  20235  rhmsubclem4  20949  lpigen  21668  psrbaglefi  22243  matvscl  22755  scmatghm  22857  slesolinv  23007  cpmatacl  23043  pnfnei  23547  mnfnei  23548  cmpcld  23729  isfildlem  24185  metrest  24852  blval2  24890  iscmet3lem2  25622  ivthlem3  25783  mbfi1fseqlem4  26048  itg2seq  26072  aalioulem6  26673  taylthlem2  26710  chpchtsum  27555  dchrmulcl  27585  bcmono  27613  nosupno  28069  nosupbday  28071  noinfno  28084  noinfbday  28086  nocvxminlem  28149  cuteq1  28212  oncutlt  28659  oniso  28666  bdayn0p1  28764  bdayfinbndlem2  28863  z12sge0  28878  cgrg3col4  29381  brbtwn2  29492  axeuclid  29550  umgredg  29725  pthdivtx  30321  pthdlem1  30361  shsvs  31934  cnlnssadj  32691  atexch  32992  mdsymlem5  33018  disjxpin  33233  fldextrspunlsplem  34355  sigaclci  34814  fnrelpredd  35776  weexenwe  35816  ptpconn  36088  satfv0  36213  satffunlem2lem1  36259  dmopab3rexdif  36260  elfuns  36773  altopth1  36826  btwnexch2  36884  ifscgr  36905  colinbtwnle  36979  trer  37200  elicc3  37201  mh-inf3f1  37425  bj-imdirval3  38214  bj-finsumval0  38315  difunieq  38406  fvineqsneu  38443  fvineqsneq  38444  poimirlem27  38674  poimir  38680  cnambfre  38695  itg2addnclem2  38699  itg2addnc  38701  areacirclem1  38735  heiborlem4  38857  elghomlem2OLD  38929  rngo2  38950  ispridl2  39081  ispridlc  39113  iss2  39385  membpartlem19  39955  paddasslem14  40999  ispsubcl2N  41113  cdleme29ex  41540  cdlemefr29exN  41568  eldiophss  43894  rencldnfilem  43936  oaabsb  44405  cantnfresb  44435  tfsconcatrn  44453  naddwordnexlem1  44508  clsk1indlem3  45152  ntrneikb  45203  mnuop3d  45364  ax6e2ndeq  45650  suctrALT2  45927  cocanss2  46030  relpmin  46050  relpfrlem  46051  2reu3  48289  iccpartiltu  48612  bgoldbtbndlem2  49012  grtrimap  49154  grimgrtri  49155  isubgr3stgrlem6  49177  isubgr3stgr  49181  pgnbgreunbgrlem1  49319  pgnbgreunbgrlem4  49325  itschlc0xyqsol1  49986  resipos  50197  elsetrecslem  50975  aacllem  51122