Theorem adantrd 491

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  im2anan9  620  jaoa  957  prlem1  1054  cad0  1618  dfsb1  2479  unineq  4247  dfopif  4830  elssabg  5293  exopxfr2  5798  tz7.7  6346  oneqmini  6373  fvun1  6934  fconst5  7162  fpropnf1  7224  f1ounsn  7229  isomin  7294  isofrlem  7297  poxp  8084  poseq  8114  tposfo2  8205  onfununi  8287  tfrlem9a  8331  oecl  8478  oawordri  8491  omwordri  8513  odi  8520  pssnn  9109  prdom2  9935  acni2  9975  cardinfima  10026  cfslb2n  10197  infpssrlem4  10235  axdc3lem4  10382  brdom6disj  10461  tskr1om  10696  indpi  10836  1idpr  10958  1re  11150  mulge0  11672  infm3  12118  uzind  12602  suprfinzcl  12624  uzwo  12846  xrlttr  13076  xmullem2  13201  snunico  13416  fzen  13478  fz0fzelfz0  13571  sqlecan  14150  hashf1lem2  14397  ccatsymb  14523  lo1le  15594  fsumss  15667  ntrivcvgfvn0  15841  fprodss  15890  smupvallem  16429  zeqzmulgcd  16456  lcmgcdlem  16552  lcmdvds  16554  lcmfunsnlem2lem1  16584  coprmproddvdslem  16608  cncongr2  16614  exprmfct  16650  infpnlem1  16857  prmdvdsprmop  16990  prmgaplem7  17004  prmlem0  17052  sscfn2  17760  isssc  17762  iszeroi  17951  funcsetcestrclem8  18103  dirge  18544  efgval  19631  dmdprd  19914  dprdw  19926  rhmsubclem4  20608  lpigen  21277  psrbaglefi  21868  matvscl  22351  scmatghm  22453  slesolinv  22600  cpmatacl  22636  pnfnei  23140  mnfnei  23141  cmpcld  23322  isfildlem  23777  metrest  24445  blval2  24483  iscmet3lem2  25225  ivthlem3  25387  mbfi1fseqlem4  25652  itg2seq  25676  aalioulem6  26278  taylthlem2  26315  chpchtsum  27163  dchrmulcl  27193  bcmono  27221  nosupno  27648  nosupbday  27650  noinfno  27663  noinfbday  27665  nocvxminlem  27723  cuteq1  27783  onscutlt  28205  onsiso  28209  bdayn0p1  28298  zs12ge0  28395  cgrg3col4  28833  brbtwn2  28885  axeuclid  28943  umgredg  29118  pthdivtx  29707  pthdlem1  29746  shsvs  31302  cnlnssadj  32059  atexch  32360  mdsymlem5  32386  disjxpin  32567  fldextrspunlsplem  33661  sigaclci  34115  fnrelpredd  35072  satfv0  35338  satffunlem2lem1  35384  dmopab3rexdif  35385  elfuns  35896  altopth1  35946  btwnexch2  36004  ifscgr  36025  colinbtwnle  36099  trer  36297  elicc3  36298  bj-imdirval3  37165  bj-finsumval0  37266  difunieq  37355  fvineqsneu  37392  fvineqsneq  37393  poimirlem27  37634  poimir  37640  cnambfre  37655  itg2addnclem2  37659  itg2addnc  37661  areacirclem1  37695  heiborlem4  37801  elghomlem2OLD  37873  rngo2  37894  ispridl2  38025  ispridlc  38057  iss2  38319  membpartlem19  38796  paddasslem14  39820  ispsubcl2N  39934  cdleme29ex  40361  cdlemefr29exN  40389  eldiophss  42755  rencldnfilem  42801  oaabsb  43276  cantnfresb  43306  tfsconcatrn  43324  naddwordnexlem1  43379  clsk1indlem3  44025  ntrneikb  44076  mnuop3d  44253  ax6e2ndeq  44542  suctrALT2  44819  relpmin  44935  relpfrlem  44936  2reu3  47104  iccpartiltu  47416  bgoldbtbndlem2  47800  grtrimap  47940  grimgrtri  47941  isubgr3stgrlem6  47963  isubgr3stgr  47967  pgnbgreunbgrlem1  48096  pgnbgreunbgrlem4  48102  itschlc0xyqsol1  48748  resipos  48956  elsetrecslem  49681  aacllem  49783