Theorem adantrd 497

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  im2anan9  632  jaoa  970  prlem1  1070  cad0  1651  dfsb1  2511  unineq  4234  dfopif  4830  elssabg  5304  exopxfr2  5822  tz7.7  6387  oneqmini  6415  fvun1  6974  fconst5  7210  fpropnf1  7269  f1ounsn  7278  isomin  7343  isofrlem  7346  poxp  8138  poseq  8168  tposfo2  8259  onfununi  8342  tfrlem9a  8387  oecl  8538  oawordri  8551  omwordri  8573  odi  8580  pssnn  9177  prdom2  10078  acni2  10118  cardinfima  10169  cfslb2n  10339  infpssrlem4  10377  axdc3lem4  10524  brdom6disj  10604  tskr1om  10845  indpi  10985  1idpr  11107  1re  11301  mulge0  11827  infm3  12269  uzind  12784  suprfinzcl  12806  uzwo  13031  xrlttr  13262  xmullem2  13388  snunico  13603  fzen  13667  fz0fzelfz0  13761  sqlecan  14346  hashf1lem2  14594  ccatsymb  14721  lo1le  15812  fsumss  15884  ntrivcvgfvn0  16061  fprodss  16108  smupvallem  16646  zeqzmulgcd  16675  lcmgcdlem  16774  lcmdvds  16776  lcmfunsnlem2lem1  16806  coprmproddvdslem  16830  cncongr2  16836  exprmfct  16873  infpnlem1  17081  prmdvdsprmop  17214  prmgaplem7  17228  prmlem0  17276  sscfn2  17986  isssc  17988  iszeroi  18177  funcsetcestrclem8  18329  dirge  18770  efgval  19924  dmdprd  20207  dprdw  20219  rhmsubclem4  20933  lpigen  21652  psrbaglefi  22227  matvscl  22739  scmatghm  22841  slesolinv  22991  cpmatacl  23027  pnfnei  23531  mnfnei  23532  cmpcld  23713  isfildlem  24169  metrest  24836  blval2  24874  iscmet3lem2  25606  ivthlem3  25767  mbfi1fseqlem4  26032  itg2seq  26056  aalioulem6  26657  taylthlem2  26694  chpchtsum  27539  dchrmulcl  27569  bcmono  27597  nosupno  28053  nosupbday  28055  noinfno  28068  noinfbday  28070  nocvxminlem  28133  cuteq1  28196  oncutlt  28643  oniso  28650  bdayn0p1  28748  bdayfinbndlem2  28847  z12sge0  28862  cgrg3col4  29365  brbtwn2  29476  axeuclid  29534  umgredg  29709  pthdivtx  30305  pthdlem1  30345  shsvs  31918  cnlnssadj  32675  atexch  32976  mdsymlem5  33002  disjxpin  33175  fldextrspunlsplem  34298  sigaclci  34757  fnrelpredd  35709  satfv0  36102  satffunlem2lem1  36148  dmopab3rexdif  36149  elfuns  36657  altopth1  36710  btwnexch2  36768  ifscgr  36789  colinbtwnle  36863  trer  37084  elicc3  37085  mh-inf3f1  37309  bj-imdirval3  38085  bj-finsumval0  38186  difunieq  38277  fvineqsneu  38314  fvineqsneq  38315  poimirlem27  38545  poimir  38551  cnambfre  38566  itg2addnclem2  38570  itg2addnc  38572  areacirclem1  38606  heiborlem4  38728  elghomlem2OLD  38800  rngo2  38821  ispridl2  38952  ispridlc  38984  iss2  39256  membpartlem19  39826  paddasslem14  40870  ispsubcl2N  40984  cdleme29ex  41411  cdlemefr29exN  41439  eldiophss  43764  rencldnfilem  43806  oaabsb  44280  cantnfresb  44310  tfsconcatrn  44328  naddwordnexlem1  44383  clsk1indlem3  45028  ntrneikb  45079  mnuop3d  45240  ax6e2ndeq  45527  suctrALT2  45804  relpmin  45920  relpfrlem  45921  2reu3  48149  iccpartiltu  48473  bgoldbtbndlem2  48873  grtrimap  49015  grimgrtri  49016  isubgr3stgrlem6  49038  isubgr3stgr  49042  pgnbgreunbgrlem1  49180  pgnbgreunbgrlem4  49186  itschlc0xyqsol1  49847  resipos  50052  elsetrecslem  50761  aacllem  50908