Theorem adantrd 492

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  im2anan9  620  jaoa  954  prlem1  1053  cad0  1619  cad0OLD  1620  dfsb1  2479  unineq  4242  dfopif  4832  elssabg  5298  exopxfr2  5805  tz7.7  6348  oneqmini  6374  fvun1  6937  fconst5  7160  fpropnf1  7219  isomin  7287  isofrlem  7290  poxp  8065  poseq  8095  tposfo2  8185  onfununi  8292  tfrlem9a  8337  oecl  8488  oawordri  8502  omwordri  8524  odi  8531  pssnn  9119  pssnnOLD  9216  prdom2  9951  acni2  9991  cardinfima  10042  cfslb2n  10213  infpssrlem4  10251  axdc3lem4  10398  brdom6disj  10477  tskr1om  10712  indpi  10852  1idpr  10974  1re  11164  mulge0  11682  infm3  12123  uzind  12604  suprfinzcl  12626  uzwo  12845  xrlttr  13069  xmullem2  13194  snunico  13406  fzen  13468  fz0fzelfz0  13557  sqlecan  14123  hashf1lem2  14367  ccatsymb  14482  lo1le  15548  fsumss  15621  ntrivcvgfvn0  15795  fprodss  15842  smupvallem  16374  zeqzmulgcd  16401  lcmgcdlem  16493  lcmdvds  16495  lcmfunsnlem2lem1  16525  coprmproddvdslem  16549  cncongr2  16555  exprmfct  16591  infpnlem1  16793  prmdvdsprmop  16926  prmgaplem7  16940  prmlem0  16989  sscfn2  17715  isssc  17717  iszeroi  17909  funcsetcestrclem8  18064  dirge  18506  efgval  19513  dmdprd  19791  dprdw  19803  lpigen  20785  psrbaglefi  21371  psrbaglefiOLD  21372  matvscl  21817  scmatghm  21919  slesolinv  22066  cpmatacl  22102  pnfnei  22608  mnfnei  22609  cmpcld  22790  isfildlem  23245  metrest  23917  blval2  23955  iscmet3lem2  24693  ivthlem3  24854  mbfi1fseqlem4  25120  itg2seq  25144  aalioulem6  25734  chpchtsum  26604  dchrmulcl  26634  bcmono  26662  nosupno  27088  nosupbday  27090  noinfno  27103  noinfbday  27105  nocvxminlem  27160  cgrg3col4  27858  brbtwn2  27917  axeuclid  27975  umgredg  28152  pthdivtx  28740  pthdlem1  28777  shsvs  30328  cnlnssadj  31085  atexch  31386  mdsymlem5  31412  disjxpin  31573  sigaclci  32820  fnrelpredd  33782  satfv0  34039  satffunlem2lem1  34085  dmopab3rexdif  34086  elfuns  34576  altopth1  34626  btwnexch2  34684  ifscgr  34705  colinbtwnle  34779  trer  34864  elicc3  34865  bj-imdirval3  35728  bj-finsumval0  35829  difunieq  35918  fvineqsneu  35955  fvineqsneq  35956  poimirlem27  36178  poimir  36184  cnambfre  36199  itg2addnclem2  36203  itg2addnc  36205  areacirclem1  36239  heiborlem4  36346  elghomlem2OLD  36418  rngo2  36439  ispridl2  36570  ispridlc  36602  iss2  36878  membpartlem19  37346  paddasslem14  38369  ispsubcl2N  38483  cdleme29ex  38910  cdlemefr29exN  38938  eldiophss  41155  rencldnfilem  41201  oaabsb  41687  cantnfresb  41717  tfsconcatrn  41735  naddwordnexlem1  41791  clsk1indlem3  42437  ntrneikb  42488  mnuop3d  42673  ax6e2ndeq  42963  suctrALT2  43241  2reu3  45462  iccpartiltu  45734  bgoldbtbndlem2  46118  rhmsubclem4  46507  itschlc0xyqsol1  46972  elsetrecslem  47264  aacllem  47368