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  623  jaoa  955  prlem1  1054  cad0  1624  cad0OLD  1625  dfsb1  2485  unineq  4168  dfopifOLD  4756  elssabg  5204  exopxfr2  5687  tz7.7  6198  oneqmini  6223  fvun1  6759  fconst5  6978  fpropnf1  7036  isomin  7103  isofrlem  7106  poxp  7848  tposfo2  7944  onfununi  8007  tfrlem9a  8051  oecl  8193  oawordri  8207  omwordri  8229  odi  8236  pssnn  8767  pssnnOLD  8815  prdom2  9506  acni2  9546  cardinfima  9597  cfslb2n  9768  infpssrlem4  9806  axdc3lem4  9953  brdom6disj  10032  tskr1om  10267  indpi  10407  1idpr  10529  1re  10719  mulge0  11236  infm3  11677  uzind  12155  suprfinzcl  12178  uzwo  12393  xrlttr  12616  xmullem2  12741  snunico  12953  fzen  13015  fz0fzelfz0  13104  sqlecan  13663  hashf1lem2  13908  ccatsymb  14025  lo1le  15101  fsumss  15175  ntrivcvgfvn0  15347  fprodss  15394  smupvallem  15926  zeqzmulgcd  15953  lcmgcdlem  16047  lcmdvds  16049  lcmfunsnlem2lem1  16079  coprmproddvdslem  16103  cncongr2  16109  exprmfct  16145  infpnlem1  16346  prmdvdsprmop  16479  prmgaplem7  16493  prmlem0  16542  sscfn2  17193  isssc  17195  iszeroi  17381  funcsetcestrclem8  17528  dirge  17963  efgval  18961  dmdprd  19239  dprdw  19251  ringadd2  19447  lpigen  20148  psrbaglefi  20745  psrbaglefiOLD  20746  matvscl  21182  scmatghm  21284  slesolinv  21431  cpmatacl  21467  pnfnei  21971  mnfnei  21972  cmpcld  22153  isfildlem  22608  metrest  23277  blval2  23315  iscmet3lem2  24044  ivthlem3  24205  mbfi1fseqlem4  24471  itg2seq  24495  aalioulem6  25085  chpchtsum  25955  dchrmulcl  25985  bcmono  26013  cgrg3col4  26799  brbtwn2  26851  axeuclid  26909  umgredg  27083  pthdivtx  27670  pthdlem1  27707  shsvs  29258  cnlnssadj  30015  atexch  30316  mdsymlem5  30342  disjxpin  30501  sigaclci  31670  fnrelpredd  32632  satfv0  32891  satffunlem2lem1  32937  dmopab3rexdif  32938  poseq  33413  nosupno  33547  nosupbday  33549  noinfno  33562  noinfbday  33564  nocvxminlem  33613  elfuns  33855  altopth1  33905  btwnexch2  33963  ifscgr  33984  colinbtwnle  34058  trer  34143  elicc3  34144  bj-imdirval3  34976  bj-finsumval0  35077  difunieq  35168  fvineqsneu  35205  fvineqsneq  35206  poimirlem27  35427  poimir  35433  cnambfre  35448  itg2addnclem2  35452  itg2addnc  35454  areacirclem1  35488  heiborlem4  35595  elghomlem2OLD  35667  rngo2  35688  ispridl2  35819  ispridlc  35851  iss2  36102  paddasslem14  37470  ispsubcl2N  37584  cdleme29ex  38011  cdlemefr29exN  38039  eldiophss  40168  rencldnfilem  40214  clsk1indlem3  41199  ntrneikb  41250  mnuop3d  41431  ax6e2ndeq  41717  suctrALT2  41995  2reu3  44135  iccpartiltu  44408  bgoldbtbndlem2  44792  rhmsubclem4  45181  itschlc0xyqsol1  45646  elsetrecslem  45857  aacllem  45958