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  1070  cad0  1648  dfsb1  2513  unineq  4241  dfopif  4835  elssabg  5313  exopxfr2  5830  tz7.7  6386  oneqmini  6414  fvun1  6972  fconst5  7204  fpropnf1  7265  f1ounsn  7270  isomin  7335  isofrlem  7338  poxp  8120  poseq  8150  tposfo2  8241  onfununi  8324  tfrlem9a  8369  oecl  8518  oawordri  8531  omwordri  8553  odi  8560  pssnn  9149  prdom2  9986  acni2  10026  cardinfima  10077  cfslb2n  10247  infpssrlem4  10285  axdc3lem4  10432  brdom6disj  10511  tskr1om  10747  indpi  10887  1idpr  11009  1re  11203  mulge0  11727  infm3  12169  uzind  12683  suprfinzcl  12705  uzwo  12930  xrlttr  13160  xmullem2  13286  snunico  13501  fzen  13564  fz0fzelfz0  13658  sqlecan  14241  hashf1lem2  14489  ccatsymb  14616  lo1le  15699  fsumss  15772  ntrivcvgfvn0  15949  fprodss  15998  smupvallem  16536  zeqzmulgcd  16563  lcmgcdlem  16659  lcmdvds  16661  lcmfunsnlem2lem1  16691  coprmproddvdslem  16715  cncongr2  16721  exprmfct  16758  infpnlem1  16965  prmdvdsprmop  17098  prmgaplem7  17112  prmlem0  17160  sscfn2  17870  isssc  17872  iszeroi  18061  funcsetcestrclem8  18213  dirge  18654  efgval  19782  dmdprd  20065  dprdw  20077  rhmsubclem4  20787  lpigen  21503  psrbaglefi  22076  matvscl  22588  scmatghm  22690  slesolinv  22837  cpmatacl  22873  pnfnei  23377  mnfnei  23378  cmpcld  23559  isfildlem  24014  metrest  24681  blval2  24719  iscmet3lem2  25451  ivthlem3  25612  mbfi1fseqlem4  25877  itg2seq  25901  aalioulem6  26500  taylthlem2  26537  chpchtsum  27383  dchrmulcl  27413  bcmono  27441  nosupno  27867  nosupbday  27869  noinfno  27882  noinfbday  27884  nocvxminlem  27947  cuteq1  28010  oncutlt  28457  oniso  28464  bdayn0p1  28562  bdayfinbndlem2  28661  z12sge0  28676  cgrg3col4  29170  brbtwn2  29255  axeuclid  29313  umgredg  29488  pthdivtx  30076  pthdlem1  30115  shsvs  31675  cnlnssadj  32432  atexch  32733  mdsymlem5  32759  disjxpin  32933  fldextrspunlsplem  34063  sigaclci  34522  fnrelpredd  35482  satfv0  35850  satffunlem2lem1  35896  dmopab3rexdif  35897  elfuns  36405  altopth1  36457  btwnexch2  36515  ifscgr  36536  colinbtwnle  36610  trer  36827  elicc3  36828  bj-imdirval3  37828  bj-finsumval0  37929  difunieq  38020  fvineqsneu  38057  fvineqsneq  38058  poimirlem27  38298  poimir  38304  cnambfre  38319  itg2addnclem2  38323  itg2addnc  38325  areacirclem1  38359  heiborlem4  38465  elghomlem2OLD  38537  rngo2  38558  ispridl2  38689  ispridlc  38721  iss2  38993  membpartlem19  39563  paddasslem14  40607  ispsubcl2N  40721  cdleme29ex  41148  cdlemefr29exN  41176  eldiophss  43505  rencldnfilem  43547  oaabsb  44021  cantnfresb  44051  tfsconcatrn  44069  naddwordnexlem1  44124  clsk1indlem3  44769  ntrneikb  44820  mnuop3d  44981  ax6e2ndeq  45268  suctrALT2  45545  relpmin  45661  relpfrlem  45662  2reu3  47847  iccpartiltu  48171  bgoldbtbndlem2  48571  grtrimap  48713  grimgrtri  48714  isubgr3stgrlem6  48736  isubgr3stgr  48740  pgnbgreunbgrlem1  48878  pgnbgreunbgrlem4  48884  itschlc0xyqsol1  49546  resipos  49753  elsetrecslem  50477  aacllem  50621