Theorem 3impia 1116

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)

Hypothesis

Ref	Expression
3impia.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Assertion

Ref	Expression
3impia	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	expimpd 454	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	3impib 1115	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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  df-3an 1088

This theorem is referenced by:  mopick2  2640  3gencl  3474  vtoclgft  3493  mob2  3651  moi  3654  reupick3  4254  disjne  4389  elpr2elpr  4800  disji2  5057  disji  5058  tz7.2  5574  sofld  6095  ordintdif  6319  funopg  6475  fvun1  6868  fvopab6  6917  fveqressseq  6966  fvcofneq  6978  fprg  7036  2f1fvneq  7142  isores3  7215  ovmpt4g  7429  ovmpos  7430  ov2gf  7431  ofrval  7554  sorpssuni  7594  sorpssint  7595  poxp  7978  suppss2  8025  frrlem12  8122  smoel  8200  smoord  8205  smogt  8207  oaass  8401  oewordi  8431  oeoalem  8436  oeoelem  8438  nnawordi  8461  nnaass  8462  qsel  8594  xpdom3  8866  onsdominel  8922  mapdom3  8945  sdomdomtrfi  8996  domsdomtrfi  8997  php  9002  onomeneq  9020  fisseneq  9043  cantnflem1  9456  ttrclss  9487  cfslbn  10032  cfsmolem  10035  cfcoflem  10037  infpssrlem4  10071  fin23lem7  10081  fin23lem25  10089  isf34lem7  10144  hsmexlem2  10192  axcc3  10203  axdc4lem  10220  tskss  10523  gruss  10561  gruurn  10563  gruiun  10564  gruel  10568  gruen  10577  grudomon  10582  grothac  10595  axpre-sup  10934  axsup  11059  addn0nid  11404  letrp1  11828  p1le  11829  lemul1a  11838  infrelb  11969  zextle  12402  zextlt  12403  btwnnz  12405  gtndiv  12406  uzind2  12422  fzind  12427  eluzsub  12623  zsupss  12686  xrltne  12906  lemaxle  12938  qbtwnre  12942  qbtwnxr  12943  xlemul1a  13031  icogelb  13139  iccleub  13143  iccsplit  13226  uzsubsubfz  13287  elfz0fzfz0  13370  difelfznle  13379  fvffz0  13383  elfzo0le  13440  fzonmapblen  13442  fzofzim  13443  ceile  13578  modadd1  13637  muladdmodid  13640  modmul1  13653  modirr  13671  fsuppmapnn0fiub0  13722  expcl2lem  13803  expclzlem  13815  expnegz  13826  leexp2r  13901  bcval4  14030  bccmpl  14032  hashbnd  14059  hashunsnggt  14118  hashgt23el  14148  elovmpowrd  14270  ccatval2  14292  ccatrcl1  14308  wrdl1s1  14328  ccat2s1fvw  14358  ccat2s1fvwOLD  14359  swrdsb0eq  14385  swrdccatin1  14447  pfxccatpfx2  14459  repswswrd  14506  cshwcsh2id  14550  absexpz  15026  climbdd  15392  iseraltlem2  15403  binomfallfac  15760  dvdsle  16028  divalgb  16122  ndvdssub  16127  dvdsgcd  16261  dfgcd2  16263  rplpwr  16276  lcmgcdlem  16320  lcmfunsn  16358  coprmdvds1  16366  qredeq  16371  2mulprm  16407  prmdvdsexpr  16431  nnnn0modprm0  16516  prm23ge5  16525  pcexp  16569  difsqpwdvds  16597  prmpwdvds  16614  ramcl  16739  cshwshashlem3  16808  cshwrepswhash1  16813  elrestr  17148  mreintcl  17313  mremre  17322  mrieqv2d  17357  initoeu2lem1  17738  funcestrcsetclem9  17874  funcsetcestrclem9  17889  prstr  18027  drsdirfi  18032  latnlej  18183  latnlej2  18186  acsdrsel  18270  acsdrscl  18273  mrelatglb  18287  mrelatlub  18289  isnmgm  18339  grpasscan1  18647  grpinvnz  18655  mulgneg2  18746  gsmsymgrfix  19045  f1omvdco2  19065  symggen  19087  odcl2  19181  odhash3  19190  lsmss1  19280  lsmss2  19282  efgred  19363  efgcpbl  19371  ablfacrp  19678  ablfac1eu  19685  ablfaclem3  19699  dvdsrmul1  19904  dvdsunit  19914  irredmul  19960  lmodlema  20137  psgnodpmr  20804  phlssphl  20873  lindsss  21040  lindfmm  21043  ply1scln0  21471  dmatelnd  21654  mdetdiaglem  21756  mdet0  21764  mdetunilem7  21776  slesolinv  21838  cramerimplem3  21843  cpmatpmat  21868  m2cpminvid2lem  21912  chfacfscmul0  22016  chfacfpmmul0  22020  riinopn  22066  clsndisj  22235  cnpf2  22410  hausnei2  22513  cmpcov  22549  cmpfii  22569  unconn  22589  t1connperf  22596  nrmr0reg  22909  fbfinnfr  23001  filuni  23045  alexsubALT  23211  tmdgsum  23255  cuspcvg  23462  mopni  23657  isngp4  23777  metdsre  24025  iimulcl  24109  phtpc01  24168  clmmulg  24273  cfilucfil4  24494  bcthlem5  24501  bcth  24502  bcth3  24504  itg1le  24887  itg2le  24913  bddmulibl  25012  bddiblnc  25015  dvnres  25104  cpnord  25108  dvnfre  25125  deg1ge  25272  dgr1term  25430  aaliou3lem2  25512  sincosq1lem  25663  cxpge0  25847  cxpmul2  25853  logrec  25922  logbgcd1irr  25953  sqfpc  26295  bcmono  26434  gausslemma2dlem1a  26522  gausslemma2dlem2  26524  gausslemma2dlem4  26526  2lgsoddprmlem3  26571  pntrmax  26721  qabvexp  26783  ostth2lem2  26791  ax5seglem4  27309  axeuclidlem  27339  uhgredgrnv  27509  usgredg4  27593  nbuhgr2vtx1edgblem  27727  vtxduhgr0e  27854  vtxduhgr0nedg  27868  rusgrpropnb  27959  uspgr2wlkeqi  28024  redwlklem  28048  lfgrwlkprop  28064  2pthnloop  28108  spthonepeq  28129  pthdlem2lem  28144  crctcshwlkn0lem3  28186  crctcshwlkn0lem5  28188  crctcshwlkn0lem7  28190  crctcshwlkn0  28195  wlkiswwlks1  28241  wlkiswwlks2  28249  wlkiswwlksupgr2  28251  wwlksnext  28267  wwlksnextproplem2  28284  wspthsnonn0vne  28291  2pthon3v  28317  rusgrnumwwlk  28349  erclwwlkeqlen  28392  erclwwlksym  28394  erclwwlktr  28395  erclwwlkneqlen  28441  erclwwlknsym  28443  erclwwlkntr  28444  uhgr3cyclex  28555  upgreupthseg  28582  eupth2lem3lem4  28604  eucrctshift  28616  4cycl2vnunb  28663  nvs  29034  nvtri  29041  nmlno0  29166  nmlnoubi  29167  ubth  29244  hlipgt0  29285  ocnel  29669  elspansn2  29938  elspansn3  29943  normcan  29947  pjoml2  29982  lecm  29988  osum  30016  nmbdfnlb  30421  leopmul  30505  hstpyth  30600  cvnbtwn  30657  ssmd1  30682  ssmd2  30683  ssdmd1  30684  ssdmd2  30685  cvmd  30707  cvdmd  30708  superpos  30725  disji2f  30925  disjif  30926  disjif2  30929  preiman0  31051  padct  31063  ffs2  31072  bcm1n  31125  s2f1  31228  omndadd  31341  ogrpaddlt  31352  archiabl  31461  slmdlema  31465  lbslsat  31708  eulerpartlemb  32344  sgn3da  32517  fisshasheq  33082  hashfundm  33083  cvmsdisj  33241  cvmlift2lem12  33285  satfrel  33338  satfrnmapom  33341  fmlasuc  33357  satffun  33380  satef  33387  sategoelfv  33391  poseq  33811  naddssim  33846  nosepon  33877  nolesgn2o  33883  nogesgn1o  33885  nosepnelem  33891  nosepne  33892  nosepdmlem  33895  nosepdm  33896  nodenselem8  33903  noresle  33909  noetasuplem4  33948  noetainflem4  33952  scutbdaylt  34021  lineintmo  34468  nn0prpwlem  34520  nn0prpw  34521  neibastop2lem  34558  lindsadd  35779  areacirc  35879  incsequz  35915  mettrifi  35924  ismtybnd  35974  heiborlem1  35978  rngoisocnv  36148  risci  36154  eqvrelqsel  36736  lfl1  37091  lkrlsp2  37124  omlfh3N  37280  cvrnbtwn  37292  cvrnbtwn2  37296  cvrnbtwn4  37300  cvlexch3  37353  cvlexch4N  37354  cvlatexchb1  37355  2llnne2N  37429  atcvrj0  37449  cvrat2  37450  ps-1  37498  3atlem5  37508  islln2a  37538  lplnriaN  37571  lplnribN  37572  llncvrlpln2  37578  lplncvrlvol2  37636  psubatN  37776  pmapglb2N  37792  pmapglb2xN  37793  2llnma1b  37807  paddasslem17  37857  pmod2iN  37870  pmodl42N  37872  hlmod1i  37877  atmod1i1  37878  atmod1i2  37880  llnmod1i2  37881  pclcmpatN  37922  osumcllem8N  37984  pexmidlem3N  37993  pl42lem4N  38003  4atexlem7  38096  ltrnnid  38157  cdlemc4  38215  cdleme32a  38462  cdlemeg46gfre  38553  cdlemf2  38583  cdlemg4c  38633  trlcoat  38744  tendovalco  38786  tendoeq2  38795  cdlemk36  38934  diael  39064  diatrl  39065  dicelval1stN  39209  dicelval2nd  39210  dihlspsnat  39354  dochkr1  39499  lcfrlem9  39571  mapdh8e  39805  hdmapval0  39854  hgmapval0  39913  nnadddir  40307  nn0rppwr  40340  nn0expgcd  40342  dvdsexpnn0  40348  incssnn0  40540  pell14qrexpcl  40696  pell14qrgap  40704  congadd  40795  acongsym  40805  acongtr  40807  dvdsacongtr  40813  jm2.19lem3  40820  jm2.19lem4  40821  jm2.26lem3  40830  ismnushort  41926  bi13impia  42115  3impcombi  42444  ioogtlb  43040  iocgtlb  43047  iocleub  43048  icoltub  43053  iooltub  43055  limclner  43199  limsupre3lem  43280  climuzlem  43291  elfzelfzlble  44824  subsubelfzo0  44829  iccpartigtl  44886  sqrtpwpw2p  45001  fmtnoprmfac1lem  45027  fmtno4prmfac  45035  evenltle  45180  even3prm2  45182  wtgoldbnnsum4prm  45265  bgoldbnnsum3prm  45267  bgoldbtbndlem1  45268  bgoldbtbndlem3  45270  bgoldbtbndlem4  45271  bgoldbtbnd  45272  upgrwlkupwlk  45313  c0snmgmhm  45483  funcringcsetcALTV2lem9  45613  funcringcsetclem9ALTV  45636  lincscmcl  45784  lindslinindimp2lem4  45813  lincresunit2  45830  lincresunit3  45833  elfzolborelfzop1  45871  m1modmmod  45878  rege1logbzge0  45916  fllog2  45925  dignn0ldlem  45959  rrx2pnecoorneor  46072  rrx2plord2  46079  rrx2linest  46099  ipolub  46285  ipoglb  46288