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 210  df-an 400

This theorem is referenced by:  im2anan9  622  jaoa  953  prlem1  1050  cad0  1619  dfsb1  2499  unineq  4204  dfopif  4760  elssabg  5203  exopxfr2  5679  tz7.7  6185  oneqmini  6210  fvun1  6729  fconst5  6945  fpropnf1  7003  isomin  7069  isofrlem  7072  poxp  7805  tposfo2  7898  onfununi  7961  tfrlem9a  8005  oecl  8145  oawordri  8159  omwordri  8181  odi  8188  pssnn  8720  prdom2  9417  acni2  9457  cardinfima  9508  cfslb2n  9679  infpssrlem4  9717  axdc3lem4  9864  brdom6disj  9943  tskr1om  10178  indpi  10318  1idpr  10440  1re  10630  mulge0  11147  infm3  11587  uzind  12062  suprfinzcl  12085  uzwo  12299  xrlttr  12521  xmullem2  12646  snunico  12857  fzen  12919  fz0fzelfz0  13008  sqlecan  13567  hashf1lem2  13810  ccatsymb  13927  lo1le  15000  fsumss  15074  ntrivcvgfvn0  15247  fprodss  15294  smupvallem  15822  zeqzmulgcd  15849  lcmgcdlem  15940  lcmdvds  15942  lcmfunsnlem2lem1  15972  coprmproddvdslem  15996  cncongr2  16002  exprmfct  16038  infpnlem1  16236  prmdvdsprmop  16369  prmgaplem7  16383  prmlem0  16431  sscfn2  17080  isssc  17082  iszeroi  17261  funcsetcestrclem8  17404  dirge  17839  efgval  18835  dmdprd  19113  dprdw  19125  ringadd2  19321  lpigen  20022  psrbaglefi  20610  matvscl  21036  scmatghm  21138  slesolinv  21285  cpmatacl  21321  pnfnei  21825  mnfnei  21826  cmpcld  22007  isfildlem  22462  metrest  23131  blval2  23169  iscmet3lem2  23896  ivthlem3  24057  mbfi1fseqlem4  24322  itg2seq  24346  aalioulem6  24933  chpchtsum  25803  dchrmulcl  25833  bcmono  25861  cgrg3col4  26647  brbtwn2  26699  axeuclid  26757  umgredg  26931  pthdivtx  27518  pthdlem1  27555  shsvs  29106  cnlnssadj  29863  atexch  30164  mdsymlem5  30190  disjxpin  30351  sigaclci  31501  fnrelpredd  32472  satfv0  32718  satffunlem2lem1  32764  dmopab3rexdif  32765  poseq  33208  nosupno  33316  nosupbday  33318  nocvxminlem  33360  elfuns  33489  altopth1  33539  btwnexch2  33597  ifscgr  33618  colinbtwnle  33692  trer  33777  elicc3  33778  bj-imdirval3  34599  bj-finsumval0  34700  difunieq  34791  fvineqsneu  34828  fvineqsneq  34829  poimirlem27  35084  poimir  35090  cnambfre  35105  itg2addnclem2  35109  itg2addnc  35111  areacirclem1  35145  heiborlem4  35252  elghomlem2OLD  35324  rngo2  35345  ispridl2  35476  ispridlc  35508  iss2  35761  paddasslem14  37129  ispsubcl2N  37243  cdleme29ex  37670  cdlemefr29exN  37698  eldiophss  39715  rencldnfilem  39761  clsk1indlem3  40746  ntrneikb  40797  mnuop3d  40979  ax6e2ndeq  41265  suctrALT2  41543  2reu3  43666  iccpartiltu  43939  bgoldbtbndlem2  44324  rhmsubclem4  44713  itschlc0xyqsol1  45180  elsetrecslem  45228  aacllem  45329