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  621  jaoa  958  prlem1  1055  cad0  1620  dfsb1  2485  unineq  4228  dfopif  4813  elssabg  5284  exopxfr2  5799  tz7.7  6349  oneqmini  6376  fvun1  6931  fconst5  7161  fpropnf1  7222  f1ounsn  7227  isomin  7292  isofrlem  7295  poxp  8078  poseq  8108  tposfo2  8199  onfununi  8281  tfrlem9a  8325  oecl  8472  oawordri  8485  omwordri  8507  odi  8514  pssnn  9103  prdom2  9928  acni2  9968  cardinfima  10019  cfslb2n  10190  infpssrlem4  10228  axdc3lem4  10375  brdom6disj  10454  tskr1om  10690  indpi  10830  1idpr  10952  1re  11144  mulge0  11668  infm3  12115  uzind  12621  suprfinzcl  12643  uzwo  12861  xrlttr  13091  xmullem2  13217  snunico  13432  fzen  13495  fz0fzelfz0  13588  sqlecan  14171  hashf1lem2  14418  ccatsymb  14545  lo1le  15614  fsumss  15687  ntrivcvgfvn0  15864  fprodss  15913  smupvallem  16452  zeqzmulgcd  16479  lcmgcdlem  16575  lcmdvds  16577  lcmfunsnlem2lem1  16607  coprmproddvdslem  16631  cncongr2  16637  exprmfct  16674  infpnlem1  16881  prmdvdsprmop  17014  prmgaplem7  17028  prmlem0  17076  sscfn2  17785  isssc  17787  iszeroi  17976  funcsetcestrclem8  18128  dirge  18569  efgval  19692  dmdprd  19975  dprdw  19987  rhmsubclem4  20665  lpigen  21333  psrbaglefi  21906  matvscl  22396  scmatghm  22498  slesolinv  22645  cpmatacl  22681  pnfnei  23185  mnfnei  23186  cmpcld  23367  isfildlem  23822  metrest  24489  blval2  24527  iscmet3lem2  25259  ivthlem3  25420  mbfi1fseqlem4  25685  itg2seq  25709  aalioulem6  26303  taylthlem2  26339  chpchtsum  27182  dchrmulcl  27212  bcmono  27240  nosupno  27667  nosupbday  27669  noinfno  27682  noinfbday  27684  nocvxminlem  27746  cuteq1  27809  oncutlt  28256  oniso  28263  bdayn0p1  28361  bdayfinbndlem2  28460  z12sge0  28475  cgrg3col4  28921  brbtwn2  28974  axeuclid  29032  umgredg  29207  pthdivtx  29795  pthdlem1  29834  shsvs  31394  cnlnssadj  32151  atexch  32452  mdsymlem5  32478  disjxpin  32658  fldextrspunlsplem  33817  sigaclci  34276  fnrelpredd  35234  satfv0  35540  satffunlem2lem1  35586  dmopab3rexdif  35587  elfuns  36095  altopth1  36147  btwnexch2  36205  ifscgr  36226  colinbtwnle  36300  trer  36498  elicc3  36499  bj-imdirval3  37498  bj-finsumval0  37599  difunieq  37690  fvineqsneu  37727  fvineqsneq  37728  poimirlem27  37968  poimir  37974  cnambfre  37989  itg2addnclem2  37993  itg2addnc  37995  areacirclem1  38029  heiborlem4  38135  elghomlem2OLD  38207  rngo2  38228  ispridl2  38359  ispridlc  38391  iss2  38665  membpartlem19  39235  paddasslem14  40279  ispsubcl2N  40393  cdleme29ex  40820  cdlemefr29exN  40848  eldiophss  43206  rencldnfilem  43248  oaabsb  43722  cantnfresb  43752  tfsconcatrn  43770  naddwordnexlem1  43825  clsk1indlem3  44470  ntrneikb  44521  mnuop3d  44698  ax6e2ndeq  44986  suctrALT2  45263  relpmin  45379  relpfrlem  45380  2reu3  47558  iccpartiltu  47882  bgoldbtbndlem2  48282  grtrimap  48424  grimgrtri  48425  isubgr3stgrlem6  48447  isubgr3stgr  48451  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem4  48595  itschlc0xyqsol1  49242  resipos  49450  elsetrecslem  50174  aacllem  50276