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  4239  dfopif  4821  elssabg  5282  exopxfr2  5787  tz7.7  6333  oneqmini  6360  fvun1  6914  fconst5  7142  fpropnf1  7204  f1ounsn  7209  isomin  7274  isofrlem  7277  poxp  8061  poseq  8091  tposfo2  8182  onfununi  8264  tfrlem9a  8308  oecl  8455  oawordri  8468  omwordri  8490  odi  8497  pssnn  9082  prdom2  9900  acni2  9940  cardinfima  9991  cfslb2n  10162  infpssrlem4  10200  axdc3lem4  10347  brdom6disj  10426  tskr1om  10661  indpi  10801  1idpr  10923  1re  11115  mulge0  11638  infm3  12084  uzind  12568  suprfinzcl  12590  uzwo  12812  xrlttr  13042  xmullem2  13167  snunico  13382  fzen  13444  fz0fzelfz0  13537  sqlecan  14116  hashf1lem2  14363  ccatsymb  14489  lo1le  15559  fsumss  15632  ntrivcvgfvn0  15806  fprodss  15855  smupvallem  16394  zeqzmulgcd  16421  lcmgcdlem  16517  lcmdvds  16519  lcmfunsnlem2lem1  16549  coprmproddvdslem  16573  cncongr2  16579  exprmfct  16615  infpnlem1  16822  prmdvdsprmop  16955  prmgaplem7  16969  prmlem0  17017  sscfn2  17725  isssc  17727  iszeroi  17916  funcsetcestrclem8  18068  dirge  18509  efgval  19596  dmdprd  19879  dprdw  19891  rhmsubclem4  20573  lpigen  21242  psrbaglefi  21833  matvscl  22316  scmatghm  22418  slesolinv  22565  cpmatacl  22601  pnfnei  23105  mnfnei  23106  cmpcld  23287  isfildlem  23742  metrest  24410  blval2  24448  iscmet3lem2  25190  ivthlem3  25352  mbfi1fseqlem4  25617  itg2seq  25641  aalioulem6  26243  taylthlem2  26280  chpchtsum  27128  dchrmulcl  27158  bcmono  27186  nosupno  27613  nosupbday  27615  noinfno  27628  noinfbday  27630  nocvxminlem  27688  cuteq1  27748  onscutlt  28170  onsiso  28174  bdayn0p1  28263  zs12ge0  28360  cgrg3col4  28798  brbtwn2  28850  axeuclid  28908  umgredg  29083  pthdivtx  29672  pthdlem1  29711  shsvs  31267  cnlnssadj  32024  atexch  32325  mdsymlem5  32351  disjxpin  32532  fldextrspunlsplem  33640  sigaclci  34099  fnrelpredd  35056  satfv0  35331  satffunlem2lem1  35377  dmopab3rexdif  35378  elfuns  35889  altopth1  35939  btwnexch2  35997  ifscgr  36018  colinbtwnle  36092  trer  36290  elicc3  36291  bj-imdirval3  37158  bj-finsumval0  37259  difunieq  37348  fvineqsneu  37385  fvineqsneq  37386  poimirlem27  37627  poimir  37633  cnambfre  37648  itg2addnclem2  37652  itg2addnc  37654  areacirclem1  37688  heiborlem4  37794  elghomlem2OLD  37866  rngo2  37887  ispridl2  38018  ispridlc  38050  iss2  38312  membpartlem19  38789  paddasslem14  39812  ispsubcl2N  39926  cdleme29ex  40353  cdlemefr29exN  40381  eldiophss  42747  rencldnfilem  42793  oaabsb  43267  cantnfresb  43297  tfsconcatrn  43315  naddwordnexlem1  43370  clsk1indlem3  44016  ntrneikb  44067  mnuop3d  44244  ax6e2ndeq  44533  suctrALT2  44810  relpmin  44926  relpfrlem  44927  2reu3  47094  iccpartiltu  47406  bgoldbtbndlem2  47790  grtrimap  47932  grimgrtri  47933  isubgr3stgrlem6  47955  isubgr3stgr  47959  pgnbgreunbgrlem1  48097  pgnbgreunbgrlem4  48103  itschlc0xyqsol1  48751  resipos  48959  elsetrecslem  49684  aacllem  49786