Theorem adantrd 494

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

Syntax hints:   → wi 4   ∧ wa 398

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 399

This theorem is referenced by:  im2anan9  621  jaoa  952  prlem1  1049  cad0  1612  dfsb1  2504  2eu3OLD  2734  unineq  4252  dfopif  4792  elssabg  5230  exopxfr2  5708  tz7.7  6210  oneqmini  6235  fvun1  6747  fconst5  6961  fpropnf1  7017  isomin  7082  isofrlem  7085  poxp  7814  tposfo2  7907  onfununi  7970  tfrlem9a  8014  oecl  8154  oawordri  8168  omwordri  8190  odi  8197  pssnn  8728  prdom2  9424  acni2  9464  cardinfima  9515  cfslb2n  9682  infpssrlem4  9720  axdc3lem4  9867  brdom6disj  9946  tskr1om  10181  indpi  10321  1idpr  10443  1re  10633  mulge0  11150  infm3  11592  uzind  12066  suprfinzcl  12089  uzwo  12303  xrlttr  12525  xmullem2  12650  snunico  12857  fzen  12916  fz0fzelfz0  13005  sqlecan  13563  hashf1lem2  13806  ccatsymb  13928  lo1le  15000  fsumss  15074  ntrivcvgfvn0  15247  fprodss  15294  smupvallem  15824  zeqzmulgcd  15851  lcmgcdlem  15942  lcmdvds  15944  lcmfunsnlem2lem1  15974  coprmproddvdslem  15998  cncongr2  16004  exprmfct  16040  infpnlem1  16238  prmdvdsprmop  16371  prmgaplem7  16385  prmlem0  16431  sscfn2  17080  isssc  17082  iszeroi  17261  funcsetcestrclem8  17404  dirge  17839  efgval  18835  dmdprd  19112  dprdw  19124  ringadd2  19317  lpigen  20021  psrbaglefi  20144  matvscl  21032  scmatghm  21134  slesolinv  21281  cpmatacl  21316  pnfnei  21820  mnfnei  21821  cmpcld  22002  isfildlem  22457  metrest  23126  blval2  23164  iscmet3lem2  23887  ivthlem3  24046  mbfi1fseqlem4  24311  itg2seq  24335  aalioulem6  24918  chpchtsum  25787  dchrmulcl  25817  bcmono  25845  cgrg3col4  26631  brbtwn2  26683  axeuclid  26741  umgredg  26915  pthdivtx  27502  pthdlem1  27539  shsvs  29092  cnlnssadj  29849  atexch  30150  mdsymlem5  30176  disjxpin  30330  sigaclci  31384  satfv0  32598  satffunlem2lem1  32644  dmopab3rexdif  32645  poseq  33088  nosupno  33196  nosupbday  33198  nocvxminlem  33240  elfuns  33369  altopth1  33419  btwnexch2  33477  ifscgr  33498  colinbtwnle  33572  trer  33657  elicc3  33658  bj-imdirval3  34466  bj-finsumval0  34559  difunieq  34647  fvineqsneu  34684  fvineqsneq  34685  poimirlem27  34911  poimir  34917  cnambfre  34932  itg2addnclem2  34936  itg2addnc  34938  areacirclem1  34974  heiborlem4  35084  elghomlem2OLD  35156  rngo2  35177  ispridl2  35308  ispridlc  35340  iss2  35593  paddasslem14  36961  ispsubcl2N  37075  cdleme29ex  37502  cdlemefr29exN  37530  eldiophss  39362  rencldnfilem  39408  clsk1indlem3  40384  ntrneikb  40435  mnuop3d  40598  ax6e2ndeq  40884  suctrALT2  41162  2reu3  43300  iccpartiltu  43573  bgoldbtbndlem2  43962  rhmsubclem4  44351  itschlc0xyqsol1  44744  elsetrecslem  44792  aacllem  44893