Theorem adantrd 496

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

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  im2anan9  631  jaoa  970  prlem1  1068  cad0  1645  dfsb1  2519  unineq  4249  dfopif  4839  elssabg  5314  exopxfr2  5831  tz7.7  6387  oneqmini  6415  fvun1  6973  fconst5  7205  fpropnf1  7266  f1ounsn  7271  isomin  7336  isofrlem  7339  poxp  8123  poseq  8153  tposfo2  8244  onfununi  8327  tfrlem9a  8372  oecl  8521  oawordri  8534  omwordri  8556  odi  8563  pssnn  9152  prdom2  9989  acni2  10029  cardinfima  10080  cfslb2n  10251  infpssrlem4  10289  axdc3lem4  10436  brdom6disj  10515  tskr1om  10751  indpi  10891  1idpr  11013  1re  11207  mulge0  11731  infm3  12173  uzind  12687  suprfinzcl  12709  uzwo  12934  xrlttr  13164  xmullem2  13290  snunico  13505  fzen  13568  fz0fzelfz0  13661  sqlecan  14244  hashf1lem2  14492  ccatsymb  14619  lo1le  15702  fsumss  15775  ntrivcvgfvn0  15952  fprodss  16001  smupvallem  16540  zeqzmulgcd  16567  lcmgcdlem  16663  lcmdvds  16665  lcmfunsnlem2lem1  16695  coprmproddvdslem  16719  cncongr2  16725  exprmfct  16762  infpnlem1  16969  prmdvdsprmop  17102  prmgaplem7  17116  prmlem0  17164  sscfn2  17874  isssc  17876  iszeroi  18065  funcsetcestrclem8  18217  dirge  18658  efgval  19786  dmdprd  20069  dprdw  20081  rhmsubclem4  20772  lpigen  21471  psrbaglefi  22044  matvscl  22556  scmatghm  22658  slesolinv  22805  cpmatacl  22841  pnfnei  23345  mnfnei  23346  cmpcld  23527  isfildlem  23982  metrest  24649  blval2  24687  iscmet3lem2  25419  ivthlem3  25580  mbfi1fseqlem4  25845  itg2seq  25869  aalioulem6  26466  taylthlem2  26502  chpchtsum  27348  dchrmulcl  27378  bcmono  27406  nosupno  27832  nosupbday  27834  noinfno  27847  noinfbday  27849  nocvxminlem  27912  cuteq1  27975  oncutlt  28422  oniso  28429  bdayn0p1  28527  bdayfinbndlem2  28626  z12sge0  28641  cgrg3col4  29124  brbtwn2  29195  axeuclid  29253  umgredg  29428  pthdivtx  30016  pthdlem1  30055  shsvs  31615  cnlnssadj  32372  atexch  32673  mdsymlem5  32699  disjxpin  32873  fldextrspunlsplem  34007  sigaclci  34466  fnrelpredd  35424  satfv0  35748  satffunlem2lem1  35794  dmopab3rexdif  35795  elfuns  36303  altopth1  36355  btwnexch2  36413  ifscgr  36434  colinbtwnle  36508  trer  36715  elicc3  36716  bj-imdirval3  37715  bj-finsumval0  37816  difunieq  37907  fvineqsneu  37944  fvineqsneq  37945  poimirlem27  38185  poimir  38191  cnambfre  38206  itg2addnclem2  38210  itg2addnc  38212  areacirclem1  38246  heiborlem4  38352  elghomlem2OLD  38424  rngo2  38445  ispridl2  38576  ispridlc  38608  iss2  38882  membpartlem19  39452  paddasslem14  40496  ispsubcl2N  40610  cdleme29ex  41037  cdlemefr29exN  41065  eldiophss  43396  rencldnfilem  43438  oaabsb  43912  cantnfresb  43942  tfsconcatrn  43960  naddwordnexlem1  44015  clsk1indlem3  44660  ntrneikb  44711  mnuop3d  44872  ax6e2ndeq  45159  suctrALT2  45436  relpmin  45552  relpfrlem  45553  2reu3  47735  iccpartiltu  48059  bgoldbtbndlem2  48459  grtrimap  48601  grimgrtri  48602  isubgr3stgrlem6  48624  isubgr3stgr  48628  pgnbgreunbgrlem1  48766  pgnbgreunbgrlem4  48772  itschlc0xyqsol1  49430  resipos  49637  elsetrecslem  50361  aacllem  50474