Theorem adantrd 483

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  syldan  486  jaoa  531  prlem1  997  cad0  1547  19.40bOLD  1805  2eu3  2543  unineq  3836  dfopif  4337  axsep  4708  elssabg  4746  exopxfr2  5188  tz7.7  5666  oneqmini  5693  suctrOLD  5726  fvun1  6179  fconst5  6376  isomin  6487  isofrlem  6490  poxp  7176  tposfo2  7262  onfununi  7325  tfrlem9a  7369  oecl  7504  oawordri  7517  omwordri  7539  odi  7546  pssnn  8063  prdom2  8712  acni2  8752  cardinfima  8803  cfslb2n  8973  infpssrlem4  9011  axdc3lem4  9158  brdom6disj  9235  tskr1om  9468  indpi  9608  1idpr  9730  1re  9918  mulge0  10425  infm3  10861  uzind  11345  suprfinzcl  11368  uzwo  11627  xrlttr  11849  xmullem2  11967  snunico  12170  fzen  12229  fz0fzelfz0  12314  sqlecan  12833  hashf1lem2  13097  lo1le  14230  fsumss  14303  ntrivcvgfvn0  14470  fprodss  14517  smupvallem  15043  zeqzmulgcd  15070  lcmgcdlem  15157  lcmdvds  15159  lcmfunsnlem2lem1  15189  coprmproddvdslem  15214  cncongr2  15220  exprmfct  15254  infpnlem1  15452  prmdvdsprmop  15585  prmgaplem7  15599  prmlem0  15650  sscfn2  16301  isssc  16303  iszeroi  16482  funcsetcestrclem8  16625  dirge  17060  efgval  17953  dmdprd  18220  dprdw  18232  ringadd2  18398  lpigen  19077  psrbaglefi  19193  matvscl  20056  scmatghm  20158  slesolinv  20305  cpmatacl  20340  pnfnei  20834  mnfnei  20835  cmpcld  21015  isfildlem  21471  metrest  22139  blval2  22177  iscmet3lem2  22898  ivthlem3  23029  mbfi1fseqlem4  23291  itg2seq  23315  dvres  23481  aalioulem6  23896  chpchtsum  24744  dchrmulcl  24774  bcmono  24802  cgrg3col4  25534  brbtwn2  25585  axeuclid  25643  umgredg  25812  usgraedgprv  25905  usgranloopv  25907  4cycl4dv  26195  0clwlk  26293  wwlkext2clwwlk  26331  frg2wot1  26584  numclwwlkun  26606  shsvs  27566  cnlnssadj  28323  atexch  28624  mdsymlem5  28650  disjxpin  28783  sigaclci  29522  poseq  30994  nocvxminlem  31089  nofulllem5  31105  elfuns  31192  altopth1  31242  btwnexch2  31300  ifscgr  31321  colinbtwnle  31395  trer  31480  elicc3  31481  bj-axsep  31981  bj-finsumval0  32324  poimirlem27  32606  poimir  32612  cnambfre  32628  itg2addnclem2  32632  itg2addnc  32634  areacirclem1  32670  heiborlem4  32783  elghomlem2OLD  32855  rngo2  32876  ispridl2  33007  ispridlc  33039  paddasslem14  34137  ispsubcl2N  34251  cdleme29ex  34680  cdlemefr29exN  34708  eldiophss  36356  rencldnfilem  36402  ioounsn  36814  clsk1indlem3  37361  ntrneikb  37412  ax6e2ndeq  37796  suctrALT2  38094  2reu3  39837  iccpartiltu  39960  bgoldbtbndlem2  40222  fpropnf1  40337  pthdivtx  40935  pthdlem1  40972  wwlksext2clwwlk  41231  clwlksfoclwwlk  41270  frgr2wwlk1  41494  fusgr2wsp2nb  41498  rhmsubclem4  41881  elsetrecslem  42243  aacllem  42356